Mathlib.Topology.MetricSpace.Basic

MetricSpace.instT0Space instance

: T0Space γ

Full source

instance (priority := 100) _root_.MetricSpace.instT0Space : T0Space γ where
  t0 _ _ h := eq_of_dist_eq_zero <| Metric.inseparable_iff.1 h

Metric Spaces are T₀ Spaces

Informal description

Every metric space is a T₀ space. That is, for any two distinct points $x$ and $y$ in a metric space $\gamma$, there exists an open set containing one of the points but not the other.

Metric.isUniformEmbedding_iff' theorem

 [PseudoMetricSpace β] {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 < δ

Full source

/-- 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. -/
theorem isUniformEmbedding_iff' [PseudoMetricSpace β] {f : γ → β} :
    IsUniformEmbeddingIsUniformEmbedding 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 < δ := by
  rw [isUniformEmbedding_iff_isUniformInducing, isUniformInducing_iff, uniformContinuous_iff]

Characterization of Uniform Embeddings in Pseudometric Spaces via $\varepsilon$-$\delta$ Conditions

Informal description

Let $\gamma$ and $\beta$ be pseudometric spaces. A map $f \colon \gamma \to \beta$ is a uniform embedding if and only if: 1. For every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $a, b \in \gamma$, if $\text{dist}(a, b) < \delta$, then $\text{dist}(f(a), f(b)) < \varepsilon$ (uniform continuity). 2. For every $\delta > 0$, there exists $\varepsilon > 0$ such that for all $a, b \in \gamma$, if $\text{dist}(f(a), f(b)) < \varepsilon$, then $\text{dist}(a, b) < \delta$ (uniform injectivity).

MetricSpace.ofT0PseudoMetricSpace abbrev

(α : Type*) [PseudoMetricSpace α] [T0Space α] : MetricSpace α

Full source

/-- If a `PseudoMetricSpace` is a T₀ space, then it is a `MetricSpace`. -/
abbrev _root_.MetricSpace.ofT0PseudoMetricSpace (α : Type*) [PseudoMetricSpace α] [T0Space α] :
    MetricSpace α where
  toPseudoMetricSpace := ‹_›
  eq_of_dist_eq_zero hdist := (Metric.inseparable_iff.2 hdist).eq

Promotion from T₀ Pseudometric Space to Metric Space

Informal description

Given a pseudometric space $\alpha$ that is also a T₀ space, the structure $\alpha$ can be promoted to a metric space.

MetricSpace.toEMetricSpace instance

: EMetricSpace γ

Full source

/-- A metric space induces an emetric space -/
instance (priority := 100) _root_.MetricSpace.toEMetricSpace : EMetricSpace γ :=
  .ofT0PseudoEMetricSpace γ

Metric Space Induces Emeric Space

Informal description

Every metric space $\gamma$ can be naturally endowed with an emetric space structure, where the extended distance function is derived from the original distance function.

Metric.isClosed_of_pairwise_le_dist theorem

{s : Set γ} {ε : ℝ} (hε : 0 < ε) (hs : s.Pairwise fun x y => ε ≤ dist x y) : IsClosed s

Full source

theorem isClosed_of_pairwise_le_dist {s : Set γ} {ε : ℝ} (hε : 0 < ε)
    (hs : s.Pairwise fun x y => ε ≤ dist x y) : IsClosed s :=
  isClosed_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hs

Closedness of $\varepsilon$-Separated Subsets in Metric Spaces

Informal description

Let $\gamma$ be a metric space, $s$ a subset of $\gamma$, and $\varepsilon$ a positive real number. If for every pair of distinct points $x, y \in s$ the distance satisfies $\varepsilon \leq \text{dist}(x, y)$, then $s$ is a closed subset of $\gamma$.

Metric.isClosedEmbedding_of_pairwise_le_dist theorem

 {α : Type*} [TopologicalSpace α] [DiscreteTopology α] {ε : ℝ} (hε : 0 < ε) {f : α → γ}
  (hf : Pairwise fun x y => ε ≤ dist (f x) (f y)) : IsClosedEmbedding f

Full source

theorem isClosedEmbedding_of_pairwise_le_dist {α : Type*} [TopologicalSpace α] [DiscreteTopology α]
    {ε : ℝ} (hε : 0 < ε) {f : α → γ} (hf : Pairwise fun x y => ε ≤ dist (f x) (f y)) :
    IsClosedEmbedding f :=
  isClosedEmbedding_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hf

Closed Embedding Criterion for $\varepsilon$-Separated Maps in Metric Spaces

Informal description

Let $\alpha$ be a topological space with the discrete topology, $\gamma$ a metric space, and $\varepsilon > 0$ a positive real number. Given a function $f \colon \alpha \to \gamma$ such that for every pair of distinct points $x, y \in \alpha$ the distance satisfies $\text{dist}(f(x), f(y)) \geq \varepsilon$, then $f$ is a closed embedding (i.e., a topological embedding with closed image).

Metric.isUniformEmbedding_bot_of_pairwise_le_dist theorem

 {β : Type*} {ε : ℝ} (hε : 0 < ε) {f : β → α} (hf : Pairwise fun x y => ε ≤ dist (f x) (f y)) :
  @IsUniformEmbedding _ _ ⊥ (by infer_instance) f

Full source

/-- 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 `β`. -/
theorem isUniformEmbedding_bot_of_pairwise_le_dist {β : Type*} {ε : ℝ} (hε : 0 < ε) {f : β → α}
    (hf : Pairwise fun x y => ε ≤ dist (f x) (f y)) :
    @IsUniformEmbedding _ _ ⊥ (by infer_instance) f :=
  isUniformEmbedding_of_spaced_out (dist_mem_uniformity hε) <| by simpa using hf

Uniform embedding criterion for $\varepsilon$-separated maps with discrete domain

Informal description

Let $\beta$ be a type, $\alpha$ a pseudometric space, and $f \colon \beta \to \alpha$ a function. Suppose there exists $\varepsilon > 0$ such that for any two distinct points $x, y \in \beta$, the distance between $f(x)$ and $f(y)$ is at least $\varepsilon$. Then $f$ is a uniform embedding when $\beta$ is equipped with the discrete uniformity.

EMetricSpace.toMetricSpaceOfDist abbrev

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

Full source

/-- 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. -/
abbrev EMetricSpace.toMetricSpaceOfDist {α : Type u} [EMetricSpace α] (dist : α → α → ℝ)
    (edist_ne_top : ∀ x y : α, edistedist x y ≠ ⊤) (h : ∀ x y, dist x y = ENNReal.toReal (edist x y)) :
    MetricSpace α :=
  @MetricSpace.ofT0PseudoMetricSpace _
    (PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist edist_ne_top h) _

Construction of Metric Space from Extended Metric Space via Distance Function

Informal description

Given an extended metric space $\alpha$ with a distance function $\mathrm{dist} : \alpha \times \alpha \to \mathbb{R}$ such that: 1. The extended distance $\mathrm{edist}(x, y)$ is finite for all $x, y \in \alpha$, 2. The distance function satisfies $\mathrm{dist}(x, y) = \mathrm{edist}(x, y).\mathrm{toReal}$ for all $x, y \in \alpha$, then $\alpha$ can be endowed with a metric space structure where the distance is given by $\mathrm{dist}$.

EMetricSpace.toMetricSpace definition

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

Full source

/-- 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. -/
def EMetricSpace.toMetricSpace {α : Type u} [EMetricSpace α] (h : ∀ x y : α, edistedist x y ≠ ⊤) :
    MetricSpace α :=
  EMetricSpace.toMetricSpaceOfDist (fun x y => ENNReal.toReal (edist x y)) h fun _ _ => rfl

Metric space induced from an extended metric space with finite distances

Informal description

Given an extended metric space $\alpha$ where the extended distance $\mathrm{edist}(x, y)$ is finite for all $x, y \in \alpha$, the space $\alpha$ can be endowed with a metric space structure by defining the distance function as $\mathrm{dist}(x, y) = \mathrm{edist}(x, y).\mathrm{toReal}$.

MetricSpace.induced abbrev

{γ β} (f : γ → β) (hf : Function.Injective f) (m : MetricSpace β) : MetricSpace γ

Full source

/-- Metric space structure pulled back by an injective function. Injectivity is necessary to
ensure that `dist x y = 0` only if `x = y`. -/
abbrev MetricSpace.induced {γ β} (f : γ → β) (hf : Function.Injective f) (m : MetricSpace β) :
    MetricSpace γ :=
  { PseudoMetricSpace.induced f m.toPseudoMetricSpace with
    eq_of_dist_eq_zero := fun h => hf (dist_eq_zero.1 h) }

Metric Space Induced by an Injective Function

Informal description

Given an injective function $f \colon \gamma \to \beta$ and a metric space structure on $\beta$, the induced metric space structure on $\gamma$ is defined by the distance function $\text{dist}(x, y) = \text{dist}(f(x), f(y))$ for all $x, y \in \gamma$. The injectivity of $f$ ensures that $\text{dist}(x, y) = 0$ if and only if $x = y$.

IsUniformEmbedding.comapMetricSpace abbrev

{α β} [UniformSpace α] [m : MetricSpace β] (f : α → β) (h : IsUniformEmbedding f) : MetricSpace α

Full source

/-- 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. -/
abbrev IsUniformEmbedding.comapMetricSpace {α β} [UniformSpace α] [m : MetricSpace β] (f : α → β)
    (h : IsUniformEmbedding f) : MetricSpace α :=
  .replaceUniformity (.induced f h.injective m) h.comap_uniformity.symm

Metric Space Pullback via Uniform Embedding

Informal description

Given a uniform space $\alpha$, a metric space $\beta$, and a uniformly embedding map $f \colon \alpha \to \beta$, the metric space structure on $\alpha$ is defined by pulling back the metric from $\beta$ via $f$. Specifically, the distance between $x, y \in \alpha$ is given by $\text{dist}(x, y) = \text{dist}(f(x), f(y))$.

Topology.IsEmbedding.comapMetricSpace abbrev

{α β} [TopologicalSpace α] [m : MetricSpace β] (f : α → β) (h : IsEmbedding f) : MetricSpace α

Full source

/-- 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. -/
abbrev Topology.IsEmbedding.comapMetricSpace {α β} [TopologicalSpace α] [m : MetricSpace β]
    (f : α → β) (h : IsEmbedding f) : MetricSpace α :=
  .replaceTopology (.induced f h.injective m) h.eq_induced

Metric Space Pullback via Topological Embedding

Informal description

Given topological spaces $\alpha$ and $\beta$, where $\beta$ is equipped with a metric space structure, and a topological embedding $f \colon \alpha \to \beta$, the metric space structure on $\alpha$ is defined by pulling back the metric from $\beta$ via $f$. Specifically, the distance between any two points $x, y \in \alpha$ is given by $\text{dist}(x, y) = \text{dist}(f(x), f(y))$.

Subtype.metricSpace instance

{α : Type*} {p : α → Prop} [MetricSpace α] : MetricSpace (Subtype p)

Full source

instance Subtype.metricSpace {α : Type*} {p : α → Prop} [MetricSpace α] :
    MetricSpace (Subtype p) :=
  .induced Subtype.val Subtype.coe_injective ‹_›

Metric Space Structure on Subtypes

Informal description

For any metric space $\alpha$ and a predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a metric space structure from $\alpha$ via the canonical embedding.

MulOpposite.instMetricSpace instance

{α : Type*} [MetricSpace α] : MetricSpace αᵐᵒᵖ

Full source

@[to_additive]
instance MulOpposite.instMetricSpace {α : Type*} [MetricSpace α] : MetricSpace αᵐᵒᵖ :=
  MetricSpace.induced MulOpposite.unop MulOpposite.unop_injective ‹_›

Metric Space Structure on the Multiplicative Opposite

Informal description

For any metric space $\alpha$, the multiplicative opposite $\alpha^\text{op}$ is also a metric space, with the distance function inherited from $\alpha$ via the canonical projection $\text{unop} : \alpha^\text{op} \to \alpha$.

Real.metricSpace instance

: MetricSpace ℝ

Full source

/-- Instantiate the reals as a metric space. -/
instance Real.metricSpace : MetricSpace ℝ := .ofT0PseudoMetricSpace ℝ

The Metric Space Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are equipped with a canonical metric space structure, where the distance function is given by $\text{dist}(x, y) = |x - y|$ for all $x, y \in \mathbb{R}$.

instMetricSpaceNNReal instance

: MetricSpace ℝ≥0

Full source

instance : MetricSpace ℝ≥0 :=
  Subtype.metricSpace

The Metric Space Structure on Non-Negative Real Numbers

Informal description

The non-negative real numbers $\mathbb{R}_{\geq 0}$ are equipped with a canonical metric space structure, inherited from the metric space structure of the real numbers.

instMetricSpaceULift instance

[MetricSpace β] : MetricSpace (ULift β)

Full source

instance [MetricSpace β] : MetricSpace (ULift β) :=
  MetricSpace.induced ULift.down ULift.down_injective ‹_›

Metric Space Structure on Lifted Types

Informal description

For any metric space $\beta$, the lifted type $\text{ULift}\,\beta$ is also a metric space, where the distance function is inherited from $\beta$ via the canonical injection $\text{ULift.down}$.

Prod.metricSpaceMax instance

[MetricSpace β] : MetricSpace (γ × β)

Full source

instance Prod.metricSpaceMax [MetricSpace β] : MetricSpace (γ × β) :=
  .ofT0PseudoMetricSpace _

Metric Space Structure on Product Spaces with Supremum Distance

Informal description

For any metric spaces $\gamma$ and $\beta$, the product space $\gamma \times \beta$ is also a metric space, where the distance between two points $(x_1, y_1)$ and $(x_2, y_2)$ is defined as the maximum of the distances $\text{dist}(x_1, x_2)$ and $\text{dist}(y_1, y_2)$.

metricSpacePi instance

: MetricSpace (∀ b, π b)

Full source

/-- A finite product of metric spaces is a metric space, with the sup distance. -/
instance metricSpacePi : MetricSpace (∀ b, π b) := .ofT0PseudoMetricSpace _

Metric Space Structure on Product Spaces with Supremum Distance

Informal description

For any family of metric spaces $\{\pi_b\}_{b \in B}$, the product space $\prod_{b \in B} \pi_b$ is a metric space with the supremum distance: for any $f, g \in \prod_{b \in B} \pi_b$, the distance is given by $\text{dist}(f, g) = \sup_{b \in B} \text{dist}(f(b), g(b))$.

Metric.secondCountable_of_countable_discretization theorem

 {α : Type u} [PseudoMetricSpace α]
  (H : ∀ ε > (0 : ℝ), ∃ (β : Type*) (_ : Encodable β) (F : α → β), ∀ x y, F x = F y → dist x y ≤ ε) :
  SecondCountableTopology α

Full source

/-- A metric space is second countable if one can reconstruct up to any `ε>0` any element of the
space from countably many data. -/
theorem secondCountable_of_countable_discretization {α : Type u} [PseudoMetricSpace α]
    (H : ∀ ε > (0 : ℝ), ∃ (β : Type*) (_ : Encodable β) (F : α → β),
      ∀ x y, F x = F y → dist x y ≤ ε) :
    SecondCountableTopology α := by
  refine secondCountable_of_almost_dense_set fun ε ε0 => ?_
  rcases H ε ε0 with ⟨β, fβ, F, hF⟩
  let Finv := rangeSplitting F
  refine ⟨range Finv, ⟨countable_range _, fun x => ?_⟩⟩
  let x' := Finv ⟨F x, mem_range_self _⟩
  have : F x' = F x := apply_rangeSplitting F _
  exact ⟨x', mem_range_self _, hF _ _ this.symm⟩

Second-Countability Criterion for Pseudometric Spaces via Countable Discretization

Informal description

Let $\alpha$ be a pseudometric space. Suppose that for every $\varepsilon > 0$, there exists an encodable type $\beta$ and a function $F : \alpha \to \beta$ such that for any $x, y \in \alpha$, if $F(x) = F(y)$ then $\text{dist}(x, y) \leq \varepsilon$. Then the topology on $\alpha$ is second-countable.

SeparationQuotient.instDist instance

{α : Type u} [PseudoMetricSpace α] : Dist (SeparationQuotient α)

Full source

instance SeparationQuotient.instDist {α : Type u} [PseudoMetricSpace α] :
    Dist (SeparationQuotient α) where
  dist := lift₂ dist fun x y x' y' hx hy ↦ by rw [dist_edist, dist_edist, ← edist_mk x,
    ← edist_mk x', mk_eq_mk.2 hx, mk_eq_mk.2 hy]

Distance Function on the Separation Quotient of a Pseudometric Space

Informal description

For any pseudometric space $\alpha$, the separation quotient of $\alpha$ is endowed with a distance function, defined as the distance between any two points in their equivalence classes.

SeparationQuotient.dist_mk theorem

{α : Type u} [PseudoMetricSpace α] (p q : α) : dist (mk p) (mk q) = dist p q

Full source

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

Distance Preservation in Separation Quotient

Informal description

For any pseudometric space $\alpha$ and any two points $p, q \in \alpha$, the distance between their images in the separation quotient is equal to the distance between $p$ and $q$ in $\alpha$, i.e., $\text{dist}(\text{mk}(p), \text{mk}(q)) = \text{dist}(p, q)$.

SeparationQuotient.instMetricSpace instance

{α : Type u} [PseudoMetricSpace α] : MetricSpace (SeparationQuotient α)

Full source

instance SeparationQuotient.instMetricSpace {α : Type u} [PseudoMetricSpace α] :
    MetricSpace (SeparationQuotient α) :=
  EMetricSpace.toMetricSpaceOfDist dist (surjective_mk.forall₂.2 edist_ne_top) <|
    surjective_mk.forall₂.2 dist_edist

Metric Space Structure on the Separation Quotient of a Pseudometric Space

Informal description

For any pseudometric space $\alpha$, the separation quotient of $\alpha$ is a metric space. The distance function on the quotient is inherited from the original pseudometric space, ensuring that the quotient space satisfies all the metric space axioms.