Documentation

Mathlib.Topology.MetricSpace.Basic

Basic properties of metric spaces, and instances. #

@[instance 100]

instance MetricSpace.instT0Space {γ : Type w} [MetricSpace γ] :

Equations

⋯ = ⋯

theorem Metric.isUniformEmbedding_iff' {β : Type v} {γ : Type w} [MetricSpace γ] [MetricSpace β] {f : γ → β} :

IsUniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ

A map between metric spaces is a uniform embedding if and only if the distance between f x and f y is controlled in terms of the distance between x and y and conversely.

@[deprecated Metric.isUniformEmbedding_iff']

theorem Metric.uniformEmbedding_iff' {β : Type v} {γ : Type w} [MetricSpace γ] [MetricSpace β] {f : γ → β} :

IsUniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, dist a b < δ → dist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, dist (f a) (f b) < ε → dist a b < δ

Alias of Metric.isUniformEmbedding_iff'.

A map between metric spaces is a uniform embedding if and only if the distance between f x and f y is controlled in terms of the distance between x and y and conversely.

@[reducible, inline]

abbrev MetricSpace.ofT0PseudoMetricSpace (α : Type u_2) [PseudoMetricSpace α] [T0Space α] :

If a PseudoMetricSpace is a T₀ space, then it is a MetricSpace.

Equations

MetricSpace.ofT0PseudoMetricSpace α = MetricSpace.mk ⋯

@[instance 100]

instance MetricSpace.toEMetricSpace {γ : Type w} [MetricSpace γ] :

EMetricSpace γ

A metric space induces an emetric space

Equations

MetricSpace.toEMetricSpace = EMetricSpace.ofT0PseudoEMetricSpace γ

theorem Metric.isClosed_of_pairwise_le_dist {γ : Type w} [MetricSpace γ] {s : Set γ} {ε : ℝ} (hε : 0 < ε) (hs : s.Pairwise fun (x y : γ) => ε ≤ dist x y) :

theorem Metric.closedEmbedding_of_pairwise_le_dist {γ : Type w} [MetricSpace γ] {α : Type u_2} [TopologicalSpace α] [DiscreteTopology α] {ε : ℝ} (hε : 0 < ε) {f : α → γ} (hf : Pairwise fun (x y : α) => ε ≤ dist (f x) (f y)) :

ClosedEmbedding f

theorem Metric.isUniformEmbedding_bot_of_pairwise_le_dist {α : Type u} [PseudoMetricSpace α] {β : Type u_2} {ε : ℝ} (hε : 0 < ε) {f : β → α} (hf : Pairwise fun (x y : β) => ε ≤ dist (f x) (f y)) :

IsUniformEmbedding f

If f : β → α sends any two distinct points to points at distance at least ε > 0, then f is a uniform embedding with respect to the discrete uniformity on β.

@[deprecated Metric.isUniformEmbedding_bot_of_pairwise_le_dist]

theorem Metric.uniformEmbedding_bot_of_pairwise_le_dist {α : Type u} [PseudoMetricSpace α] {β : Type u_2} {ε : ℝ} (hε : 0 < ε) {f : β → α} (hf : Pairwise fun (x y : β) => ε ≤ dist (f x) (f y)) :

IsUniformEmbedding f

Alias of Metric.isUniformEmbedding_bot_of_pairwise_le_dist.

If f : β → α sends any two distinct points to points at distance at least ε > 0, then f is a uniform embedding with respect to the discrete uniformity on β.

@[reducible, inline]

abbrev EMetricSpace.toMetricSpaceOfDist {α : Type u} [EMetricSpace α] (dist : α → α → ℝ) (edist_ne_top : ∀ (x y : α), edist x y ≠ ⊤) (h : ∀ (x y : α), dist x y = (edist x y).toReal) :

One gets a metric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the metric space and the emetric space. In this definition, the distance is given separately, to be able to prescribe some expression which is not defeq to the push-forward of the edistance to reals.

Equations

EMetricSpace.toMetricSpaceOfDist dist edist_ne_top h = MetricSpace.ofT0PseudoMetricSpace α

def EMetricSpace.toMetricSpace {α : Type u} [EMetricSpace α] (h : ∀ (x y : α), edist x y ≠ ⊤) :

One gets a metric space from an emetric space if the edistance is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the uniformity are defeq in the metric space and the emetric space.

Equations

EMetricSpace.toMetricSpace h = EMetricSpace.toMetricSpaceOfDist (fun (x y : α) => (edist x y).toReal) h ⋯

@[reducible, inline]

abbrev MetricSpace.induced {γ : Type u_2} {β : Type u_3} (f : γ → β) (hf : Function.Injective f) (m : MetricSpace β) :

Metric space structure pulled back by an injective function. Injectivity is necessary to ensure that dist x y = 0 only if x = y.

Equations

MetricSpace.induced f hf m = MetricSpace.mk ⋯

@[reducible, inline]

abbrev IsUniformEmbedding.comapMetricSpace {α : Type u_2} {β : Type u_3} [UniformSpace α] [m : MetricSpace β] (f : α → β) (h : IsUniformEmbedding f) :

Pull back a metric space structure by a uniform embedding. This is a version of MetricSpace.induced useful in case if the domain already has a UniformSpace structure.

Equations

IsUniformEmbedding.comapMetricSpace f h = (MetricSpace.induced f ⋯ m).replaceUniformity ⋯

@[deprecated IsUniformEmbedding.comapMetricSpace]

def UniformEmbedding.comapMetricSpace {α : Type u_2} {β : Type u_3} [UniformSpace α] [m : MetricSpace β] (f : α → β) (h : IsUniformEmbedding f) :

Alias of IsUniformEmbedding.comapMetricSpace.

Pull back a metric space structure by a uniform embedding. This is a version of MetricSpace.induced useful in case if the domain already has a UniformSpace structure.

Equations

@UniformEmbedding.comapMetricSpace = @IsUniformEmbedding.comapMetricSpace

@[reducible, inline]

abbrev Embedding.comapMetricSpace {α : Type u_2} {β : Type u_3} [TopologicalSpace α] [m : MetricSpace β] (f : α → β) (h : Embedding f) :

Pull back a metric space structure by an embedding. This is a version of MetricSpace.induced useful in case if the domain already has a TopologicalSpace structure.

Equations

Embedding.comapMetricSpace f h = (MetricSpace.induced f ⋯ m).replaceTopology ⋯

instance Subtype.metricSpace {α : Type u_2} {p : α → Prop} [MetricSpace α] :

MetricSpace (Subtype p)

Equations

Subtype.metricSpace = MetricSpace.induced Subtype.val ⋯ inst

instance instMetricSpaceAddOpposite {α : Type u_2} [MetricSpace α] :

MetricSpace αᵃᵒᵖ

Equations

instMetricSpaceAddOpposite = MetricSpace.induced AddOpposite.unop ⋯ inst

instance instMetricSpaceMulOpposite {α : Type u_2} [MetricSpace α] :

MetricSpace αᵐᵒᵖ

Equations

instMetricSpaceMulOpposite = MetricSpace.induced MulOpposite.unop ⋯ inst

instance Real.metricSpace :

MetricSpace ℝ

Instantiate the reals as a metric space.

Equations

Real.metricSpace = MetricSpace.ofT0PseudoMetricSpace ℝ

instance instMetricSpaceNNReal :

MetricSpace NNReal

Equations

instMetricSpaceNNReal = Subtype.metricSpace

instance instMetricSpaceULift {β : Type v} [MetricSpace β] :

MetricSpace (ULift.{u_2, v} β)

Equations

instMetricSpaceULift = MetricSpace.induced ULift.down ⋯ inst

instance Prod.metricSpaceMax {β : Type v} {γ : Type w} [MetricSpace γ] [MetricSpace β] :

MetricSpace (γ × β)

Equations

Prod.metricSpaceMax = MetricSpace.ofT0PseudoMetricSpace (γ × β)

instance metricSpacePi {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → MetricSpace (π b)] :

MetricSpace ((b : β) → π b)

A finite product of metric spaces is a metric space, with the sup distance.

Equations

metricSpacePi = MetricSpace.ofT0PseudoMetricSpace ((b : β) → π b)

theorem Metric.secondCountable_of_countable_discretization {α : Type u} [MetricSpace α] (H : ∀ ε > 0, ∃ (β : Type u_2) (x : Encodable β) (F : α → β), ∀ (x y : α), F x = F y → dist x y ≤ ε) :

SecondCountableTopology α

A metric space is second countable if one can reconstruct up to any ε>0 any element of the space from countably many data.

instance SeparationQuotient.instDist {α : Type u} [PseudoMetricSpace α] :

Dist (SeparationQuotient α)

Equations

SeparationQuotient.instDist = { dist := SeparationQuotient.lift₂ dist ⋯ }

theorem SeparationQuotient.dist_mk {α : Type u} [PseudoMetricSpace α] (p : α) (q : α) :

dist (SeparationQuotient.mk p) (SeparationQuotient.mk q) = dist p q

instance SeparationQuotient.instMetricSpace {α : Type u} [PseudoMetricSpace α] :

MetricSpace (SeparationQuotient α)

Equations

SeparationQuotient.instMetricSpace = EMetricSpace.toMetricSpaceOfDist dist ⋯ ⋯

`Additive`, `Multiplicative` #

The distance on those type synonyms is inherited without change.

instance instMetricSpaceAdditive_1 {X : Type u_1} [MetricSpace X] :

MetricSpace (Additive X)

Equations

instMetricSpaceAdditive_1 = inst

instance instMetricSpaceMultiplicative_1 {X : Type u_1} [MetricSpace X] :

MetricSpace (Multiplicative X)

Equations

instMetricSpaceMultiplicative_1 = inst

instance MulOpposite.instMetricSpace {X : Type u_1} [MetricSpace X] :

MetricSpace Xᵐᵒᵖ

Equations

MulOpposite.instMetricSpace = MetricSpace.induced MulOpposite.unop ⋯ inst

Order dual #

The distance on this type synonym is inherited without change.

instance instMetricSpaceOrderDual_1 {X : Type u_1} [MetricSpace X] :

MetricSpace Xᵒᵈ

Equations

instMetricSpaceOrderDual_1 = inst