Basic properties of metric spaces, and instances.

@[instance 100]

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

Equations

• ⋯ = ⋯

theorem Metric.uniformEmbedding_iff' {β : Type v} {γ : Type w} [MetricSpace γ] [MetricSpace β] {f : γ → β} : UniformEmbedding 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.

@[reducible, inline]

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

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) : IsClosed s

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.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)) : UniformEmbedding 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 β.

@[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) : MetricSpace α

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 ≠ ⊤) : MetricSpace α

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 β) : 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 UniformEmbedding.comapMetricSpace {α : Type u_2} {β : Type u_3} [UniformSpace α] [m : MetricSpace β] (f : α → β) (h : UniformEmbedding f) : MetricSpace α

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 f h = (MetricSpace.induced f ⋯ m).replaceUniformity ⋯

@[reducible, inline]

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

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