Metric spaces

This file defines metric spaces. Many definitions and theorems expected on metric spaces are already introduced on uniform spaces and topological spaces. For example: open and closed sets, compactness, completeness, continuity and uniform continuity

Main definitions

• Dist α: Endows a space α with a function dist a b.
• PseudoMetricSpace α: A space endowed with a distance function, which can be zero even if the two elements are non-equal.
• Metric.ball x ε: The set of all points y with dist y x < ε.
• Metric.Bounded s: Whether a subset of a PseudoMetricSpace is bounded.
• MetricSpace α: A PseudoMetricSpace with the guarantee dist x y = 0 → x = y.

Additional useful definitions:

• nndist a b: dist as a function to the non-negative reals.
• Metric.closedBall x ε: The set of all points y with dist y x ≤ ε.
• Metric.sphere x ε: The set of all points y with dist y x = ε.
• ProperSpace α: A PseudoMetricSpace where all closed balls are compact.
• Metric.diam s : The iSup of the distances of members of s. Defined in terms of EMetric.diam, for better handling of the case when it should be infinite.

TODO (anyone): Add "Main results" section.

Implementation notes

Since a lot of elementary properties don't require eq_of_dist_eq_zero we start setting up the theory of PseudoMetricSpace, where we don't require dist x y = 0 → x = y and we specialize to MetricSpace at the end.

Tags

metric, pseudo_metric, dist

def UniformSpace.ofDist {α : Type u} (dist : α → α → ℝ) (dist_self : ∀ (x : α), dist x x = 0) (dist_comm : ∀ (x y : α), dist x y = dist y x) (dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z) : UniformSpace α

Construct a uniform structure from a distance function and metric space axioms

Equations

• UniformSpace.ofDist dist dist_self dist_comm dist_triangle = UniformSpace.ofFun dist dist_self dist_comm dist_triangle UniformSpace.ofDist.proof_1

@[reducible]

def Bornology.ofDist {α : Type u_3} (dist : α → α → ℝ) (dist_comm : ∀ (x y : α), dist x y = dist y x) (dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z) : Bornology α

Construct a bornology from a distance function and metric space axioms.

Equations

• One or more equations did not get rendered due to their size.

theorem Dist.ext_iff {α : Type u_3} (x : Dist α) (y : Dist α) : x = y ↔ dist = dist

theorem Dist.ext {α : Type u_3} (x : Dist α) (y : Dist α) (dist : dist = dist) : x = y

class Dist (α : Type u_3) : Type u_3

• dist : α → α → ℝ

The distance function (given an ambient metric space on α), which returns a nonnegative real number dist x y given x y : α.

class PseudoMetricSpace (α : Type u) extends Dist : Type u

• dist : α → α → ℝ
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s_1 | ∃ C, ∀ (x : α), x ∈ s_1ᶜ → ∀ (y : α), y ∈ s_1ᶜ → dist x y ≤ C}

Pseudo metric and Metric spaces

A pseudo metric space is endowed with a distance for which the requirement d(x,y)=0 → x = y might not hold. A metric space is a pseudo metric space such that d(x,y)=0 → x = y. Each pseudo metric space induces a canonical UniformSpace and hence a canonical TopologicalSpace This is enforced in the type class definition, by extending the UniformSpace structure. When instantiating a PseudoMetricSpace structure, the uniformity fields are not necessary, they will be filled in by default. In the same way, each (pseudo) metric space induces a (pseudo) emetric space structure. It is included in the structure, but filled in by default.

theorem PseudoMetricSpace.ext {α : Type u_3} {m : PseudoMetricSpace α} {m' : PseudoMetricSpace α} (h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist) : m = m'

Two pseudo metric space structures with the same distance function coincide.

instance PseudoMetricSpace.toEDist {α : Type u} [PseudoMetricSpace α] : EDist α

Equations

• PseudoMetricSpace.toEDist = { edist := PseudoMetricSpace.edist }

def PseudoMetricSpace.ofDistTopology {α : Type u} [TopologicalSpace α] (dist : α → α → ℝ) (dist_self : ∀ (x : α), dist x x = 0) (dist_comm : ∀ (x y : α), dist x y = dist y x) (dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z) (H : ∀ (s : Set α), IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : α), dist x y < ε → y ∈ s) : PseudoMetricSpace α

Construct a pseudo-metric space structure whose underlying topological space structure (definitionally) agrees which a pre-existing topology which is compatible with a given distance function.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem dist_self {α : Type u} [PseudoMetricSpace α] (x : α) : dist x x = 0

theorem dist_comm {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : dist x y = dist y x

theorem edist_dist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : edist x y = ENNReal.ofReal (dist x y)

theorem dist_triangle {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) : dist x z ≤ dist x y + dist y z

theorem dist_triangle_left {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) : dist x y ≤ dist z x + dist z y

theorem dist_triangle_right {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) : dist x y ≤ dist x z + dist y z

theorem dist_triangle4 {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) (w : α) : dist x w ≤ dist x y + dist y z + dist z w

theorem dist_triangle4_left {α : Type u} [PseudoMetricSpace α] (x₁ : α) (y₁ : α) (x₂ : α) (y₂ : α) : dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)

theorem dist_triangle4_right {α : Type u} [PseudoMetricSpace α] (x₁ : α) (y₁ : α) (x₂ : α) (y₂ : α) : dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂

theorem dist_le_Ico_sum_dist {α : Type u} [PseudoMetricSpace α] (f : ℕ → α) {m : ℕ} {n : ℕ} (h : m ≤ n) : dist (f m) (f n) ≤ Finset.sum (Finset.Ico m n) fun i => dist (f i) (f (i + 1))

The triangle (polygon) inequality for sequences of points; Finset.Ico version.

theorem dist_le_range_sum_dist {α : Type u} [PseudoMetricSpace α] (f : ℕ → α) (n : ℕ) : dist (f 0) (f n) ≤ Finset.sum (Finset.range n) fun i => dist (f i) (f (i + 1))

The triangle (polygon) inequality for sequences of points; Finset.range version.

theorem dist_le_Ico_sum_of_dist_le {α : Type u} [PseudoMetricSpace α] {f : ℕ → α} {m : ℕ} {n : ℕ} (hmn : m ≤ n) {d : ℕ → ℝ} (hd : ∀ {k : ℕ}, m ≤ k → k < n → dist (f k) (f (k + 1)) ≤ d k) : dist (f m) (f n) ≤ Finset.sum (Finset.Ico m n) fun i => d i

A version of dist_le_Ico_sum_dist with each intermediate distance replaced with an upper estimate.

theorem dist_le_range_sum_of_dist_le {α : Type u} [PseudoMetricSpace α] {f : ℕ → α} (n : ℕ) {d : ℕ → ℝ} (hd : ∀ {k : ℕ}, k < n → dist (f k) (f (k + 1)) ≤ d k) : dist (f 0) (f n) ≤ Finset.sum (Finset.range n) fun i => d i

A version of dist_le_range_sum_dist with each intermediate distance replaced with an upper estimate.

theorem swap_dist {α : Type u} [PseudoMetricSpace α] : Function.swap dist = dist

theorem abs_dist_sub_le {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) : |dist x z - dist y z| ≤ dist x y

theorem dist_nonneg {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} : 0 ≤ dist x y

def Mathlib.Meta.Positivity.evalDist : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: distances are nonnegative.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem abs_dist {α : Type u} [PseudoMetricSpace α] {a : α} {b : α} : |dist a b| = dist a b

class NNDist (α : Type u_3) : Type u_3

• nndist : α → α → NNReal

A version of Dist that takes value in ℝ≥0.

instance PseudoMetricSpace.toNNDist {α : Type u} [PseudoMetricSpace α] : NNDist α

Distance as a nonnegative real number.

Equations

• PseudoMetricSpace.toNNDist = { nndist := fun a b => { val := dist a b, property := (_ : 0 ≤ dist a b) } }

theorem dist_nndist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : dist x y = ↑(nndist x y)

Express dist in terms of nndist

@[simp]

theorem coe_nndist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : ↑(nndist x y) = dist x y

theorem edist_nndist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : edist x y = ↑(nndist x y)

Express edist in terms of nndist

theorem nndist_edist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : nndist x y = ENNReal.toNNReal (edist x y)

Express nndist in terms of edist

@[simp]

theorem coe_nnreal_ennreal_nndist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : ↑(nndist x y) = edist x y

@[simp]

theorem edist_lt_coe {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {c : NNReal} : edist x y < ↑c ↔ nndist x y < c

@[simp]

theorem edist_le_coe {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {c : NNReal} : edist x y ≤ ↑c ↔ nndist x y ≤ c

theorem edist_lt_top {α : Type u_3} [PseudoMetricSpace α] (x : α) (y : α) : edist x y < ⊤

In a pseudometric space, the extended distance is always finite

theorem edist_ne_top {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : edist x y ≠ ⊤

In a pseudometric space, the extended distance is always finite

@[simp]

theorem nndist_self {α : Type u} [PseudoMetricSpace α] (a : α) : nndist a a = 0

nndist x x vanishes

@[simp]

theorem dist_lt_coe {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {c : NNReal} : dist x y < ↑c ↔ nndist x y < c

@[simp]

theorem dist_le_coe {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {c : NNReal} : dist x y ≤ ↑c ↔ nndist x y ≤ c

@[simp]

theorem edist_lt_ofReal {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {r : ℝ} : edist x y < ENNReal.ofReal r ↔ dist x y < r

@[simp]

theorem edist_le_ofReal {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {r : ℝ} (hr : 0 ≤ r) : edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r

theorem nndist_dist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : nndist x y = Real.toNNReal (dist x y)

Express nndist in terms of dist

theorem nndist_comm {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : nndist x y = nndist y x

theorem nndist_triangle {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) : nndist x z ≤ nndist x y + nndist y z

Triangle inequality for the nonnegative distance

theorem nndist_triangle_left {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) : nndist x y ≤ nndist z x + nndist z y

theorem nndist_triangle_right {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) : nndist x y ≤ nndist x z + nndist y z

theorem dist_edist {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : dist x y = ENNReal.toReal (edist x y)

Express dist in terms of edist

def Metric.ball {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α

ball x ε is the set of all points y with dist y x < ε

Equations

• Metric.ball x ε = {y | dist y x < ε}

@[simp]

theorem Metric.mem_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} : y ∈ Metric.ball x ε ↔ dist y x < ε

theorem Metric.mem_ball' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} : y ∈ Metric.ball x ε ↔ dist x y < ε

theorem Metric.pos_of_mem_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} (hy : y ∈ Metric.ball x ε) : 0 < ε

theorem Metric.mem_ball_self {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 < ε) : x ∈ Metric.ball x ε

@[simp]

theorem Metric.nonempty_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Set.Nonempty (Metric.ball x ε) ↔ 0 < ε

@[simp]

theorem Metric.ball_eq_empty {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε = ∅ ↔ ε ≤ 0

@[simp]

theorem Metric.ball_zero {α : Type u} [PseudoMetricSpace α] {x : α} : Metric.ball x 0 = ∅

theorem Metric.exists_lt_mem_ball_of_mem_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} (h : x ∈ Metric.ball y ε) : ∃ ε', ε' < ε ∧ x ∈ Metric.ball y ε'

If a point belongs to an open ball, then there is a strictly smaller radius whose ball also contains it.

See also exists_lt_subset_ball.

theorem Metric.ball_eq_ball {α : Type u} [PseudoMetricSpace α] (ε : ℝ) (x : α) : UniformSpace.ball x {p | dist p.snd p.fst < ε} = Metric.ball x ε

theorem Metric.ball_eq_ball' {α : Type u} [PseudoMetricSpace α] (ε : ℝ) (x : α) : UniformSpace.ball x {p | dist p.fst p.snd < ε} = Metric.ball x ε

@[simp]

theorem Metric.iUnion_ball_nat {α : Type u} [PseudoMetricSpace α] (x : α) : ⋃ (n : ℕ), Metric.ball x ↑n = Set.univ

@[simp]

theorem Metric.iUnion_ball_nat_succ {α : Type u} [PseudoMetricSpace α] (x : α) : ⋃ (n : ℕ), Metric.ball x (↑n + 1) = Set.univ

def Metric.closedBall {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α

closedBall x ε is the set of all points y with dist y x ≤ ε

Equations

• Metric.closedBall x ε = {y | dist y x ≤ ε}

@[simp]

theorem Metric.mem_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} : y ∈ Metric.closedBall x ε ↔ dist y x ≤ ε

theorem Metric.mem_closedBall' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} : y ∈ Metric.closedBall x ε ↔ dist x y ≤ ε

def Metric.sphere {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) : Set α

sphere x ε is the set of all points y with dist y x = ε

Equations

• Metric.sphere x ε = {y | dist y x = ε}

@[simp]

theorem Metric.mem_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} : y ∈ Metric.sphere x ε ↔ dist y x = ε

theorem Metric.mem_sphere' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} : y ∈ Metric.sphere x ε ↔ dist x y = ε

theorem Metric.ne_of_mem_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} (h : y ∈ Metric.sphere x ε) (hε : ε ≠ 0) : y ≠ x

theorem Metric.nonneg_of_mem_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} (hy : y ∈ Metric.sphere x ε) : 0 ≤ ε

@[simp]

theorem Metric.sphere_eq_empty_of_neg {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (hε : ε < 0) : Metric.sphere x ε = ∅

theorem Metric.sphere_eq_empty_of_subsingleton {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (hε : ε ≠ 0) : Metric.sphere x ε = ∅

theorem Metric.sphere_isEmpty_of_subsingleton {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (hε : ε ≠ 0) : IsEmpty ↑(Metric.sphere x ε)

theorem Metric.mem_closedBall_self {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 ≤ ε) : x ∈ Metric.closedBall x ε

@[simp]

theorem Metric.nonempty_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Set.Nonempty (Metric.closedBall x ε) ↔ 0 ≤ ε

@[simp]

theorem Metric.closedBall_eq_empty {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε = ∅ ↔ ε < 0

theorem Metric.closedBall_eq_sphere_of_nonpos {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (hε : ε ≤ 0) : Metric.closedBall x ε = Metric.sphere x ε

Closed balls and spheres coincide when the radius is non-positive

theorem Metric.ball_subset_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ⊆ Metric.closedBall x ε

theorem Metric.sphere_subset_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.sphere x ε ⊆ Metric.closedBall x ε

theorem Metric.closedBall_disjoint_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {δ : ℝ} {ε : ℝ} (h : δ + ε ≤ dist x y) : Disjoint (Metric.closedBall x δ) (Metric.ball y ε)

theorem Metric.ball_disjoint_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {δ : ℝ} {ε : ℝ} (h : δ + ε ≤ dist x y) : Disjoint (Metric.ball x δ) (Metric.closedBall y ε)

theorem Metric.ball_disjoint_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {δ : ℝ} {ε : ℝ} (h : δ + ε ≤ dist x y) : Disjoint (Metric.ball x δ) (Metric.ball y ε)

theorem Metric.closedBall_disjoint_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {δ : ℝ} {ε : ℝ} (h : δ + ε < dist x y) : Disjoint (Metric.closedBall x δ) (Metric.closedBall y ε)

theorem Metric.sphere_disjoint_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Disjoint (Metric.sphere x ε) (Metric.ball x ε)

@[simp]

theorem Metric.ball_union_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ∪ Metric.sphere x ε = Metric.closedBall x ε

@[simp]

theorem Metric.sphere_union_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.sphere x ε ∪ Metric.ball x ε = Metric.closedBall x ε

@[simp]

theorem Metric.closedBall_diff_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε \ Metric.sphere x ε = Metric.ball x ε

@[simp]

theorem Metric.closedBall_diff_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε \ Metric.ball x ε = Metric.sphere x ε

theorem Metric.mem_ball_comm {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} : x ∈ Metric.ball y ε ↔ y ∈ Metric.ball x ε

theorem Metric.mem_closedBall_comm {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} : x ∈ Metric.closedBall y ε ↔ y ∈ Metric.closedBall x ε

theorem Metric.mem_sphere_comm {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} : x ∈ Metric.sphere y ε ↔ y ∈ Metric.sphere x ε

theorem Metric.ball_subset_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : ε₁ ≤ ε₂) : Metric.ball x ε₁ ⊆ Metric.ball x ε₂

theorem Metric.closedBall_eq_bInter_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.closedBall x ε = ⋂ (δ : ℝ) (_ : δ > ε), Metric.ball x δ

theorem Metric.ball_subset_ball' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : ε₁ + dist x y ≤ ε₂) : Metric.ball x ε₁ ⊆ Metric.ball y ε₂

theorem Metric.closedBall_subset_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : ε₁ ≤ ε₂) : Metric.closedBall x ε₁ ⊆ Metric.closedBall x ε₂

theorem Metric.closedBall_subset_closedBall' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : ε₁ + dist x y ≤ ε₂) : Metric.closedBall x ε₁ ⊆ Metric.closedBall y ε₂

theorem Metric.closedBall_subset_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : ε₁ < ε₂) : Metric.closedBall x ε₁ ⊆ Metric.ball x ε₂

theorem Metric.closedBall_subset_ball' {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : ε₁ + dist x y < ε₂) : Metric.closedBall x ε₁ ⊆ Metric.ball y ε₂

theorem Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : Set.Nonempty (Metric.closedBall x ε₁ ∩ Metric.closedBall y ε₂)) : dist x y ≤ ε₁ + ε₂

theorem Metric.dist_lt_add_of_nonempty_closedBall_inter_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : Set.Nonempty (Metric.closedBall x ε₁ ∩ Metric.ball y ε₂)) : dist x y < ε₁ + ε₂

theorem Metric.dist_lt_add_of_nonempty_ball_inter_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : Set.Nonempty (Metric.ball x ε₁ ∩ Metric.closedBall y ε₂)) : dist x y < ε₁ + ε₂

theorem Metric.dist_lt_add_of_nonempty_ball_inter_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : Set.Nonempty (Metric.ball x ε₁ ∩ Metric.ball y ε₂)) : dist x y < ε₁ + ε₂

@[simp]

theorem Metric.iUnion_closedBall_nat {α : Type u} [PseudoMetricSpace α] (x : α) : ⋃ (n : ℕ), Metric.closedBall x ↑n = Set.univ

theorem Metric.iUnion_inter_closedBall_nat {α : Type u} [PseudoMetricSpace α] (s : Set α) (x : α) : ⋃ (n : ℕ), s ∩ Metric.closedBall x ↑n = s

theorem Metric.ball_subset {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε₁ : ℝ} {ε₂ : ℝ} (h : dist x y ≤ ε₂ - ε₁) : Metric.ball x ε₁ ⊆ Metric.ball y ε₂

theorem Metric.ball_half_subset {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (y : α) (h : y ∈ Metric.ball x (ε / 2)) : Metric.ball y (ε / 2) ⊆ Metric.ball x ε

theorem Metric.exists_ball_subset_ball {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {ε : ℝ} (h : y ∈ Metric.ball x ε) : ∃ ε', ε' > 0 ∧ Metric.ball y ε' ⊆ Metric.ball x ε

theorem Metric.forall_of_forall_mem_closedBall {α : Type u} [PseudoMetricSpace α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in Filter.atTop, (y : α) → y ∈ Metric.closedBall x R → p y) (y : α) : p y

If a property holds for all points in closed balls of arbitrarily large radii, then it holds for all points.

theorem Metric.forall_of_forall_mem_ball {α : Type u} [PseudoMetricSpace α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in Filter.atTop, (y : α) → y ∈ Metric.ball x R → p y) (y : α) : p y

If a property holds for all points in balls of arbitrarily large radii, then it holds for all points.

theorem Metric.isBounded_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C

theorem Metric.isBounded_iff_eventually {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded s ↔ ∀ᶠ (C : ℝ) in Filter.atTop, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C

theorem Metric.isBounded_iff_exists_ge {α : Type u} [PseudoMetricSpace α] {s : Set α} (c : ℝ) : Bornology.IsBounded s ↔ ∃ C, c ≤ C ∧ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C

theorem Metric.isBounded_iff_nndist {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded s ↔ ∃ C, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist x y ≤ C

theorem Metric.toUniformSpace_eq {α : Type u} [PseudoMetricSpace α] : PseudoMetricSpace.toUniformSpace = UniformSpace.ofDist dist (_ : ∀ (x : α), dist x x = 0) (_ : ∀ (x y : α), dist x y = dist y x) (_ : ∀ (x y z : α), dist x z ≤ dist x y + dist y z)

theorem Metric.uniformity_basis_dist {α : Type u} [PseudoMetricSpace α] : Filter.HasBasis (uniformity α) (fun ε => 0 < ε) fun ε => {p | dist p.fst p.snd < ε}

theorem Metric.mk_uniformity_basis {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ} (hf₀ : ∀ (i : β), p i → 0 < f i) (hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε) : Filter.HasBasis (uniformity α) p fun i => {p | dist p.fst p.snd < f i}

Given f : β → ℝ, if f sends {i | p i} to a set of positive numbers accumulating to zero, then f i-neighborhoods of the diagonal form a basis of 𝓤 α.

For specific bases see uniformity_basis_dist, uniformity_basis_dist_inv_nat_succ, and uniformity_basis_dist_inv_nat_pos.

theorem Metric.uniformity_basis_dist_rat {α : Type u} [PseudoMetricSpace α] : Filter.HasBasis (uniformity α) (fun r => 0 < r) fun r => {p | dist p.fst p.snd < ↑r}

theorem Metric.uniformity_basis_dist_inv_nat_succ {α : Type u} [PseudoMetricSpace α] : Filter.HasBasis (uniformity α) (fun x => True) fun n => {p | dist p.fst p.snd < 1 / (↑n + 1)}

theorem Metric.uniformity_basis_dist_inv_nat_pos {α : Type u} [PseudoMetricSpace α] : Filter.HasBasis (uniformity α) (fun n => 0 < n) fun n => {p | dist p.fst p.snd < 1 / ↑n}

theorem Metric.uniformity_basis_dist_pow {α : Type u} [PseudoMetricSpace α] {r : ℝ} (h0 : 0 < r) (h1 : r < 1) : Filter.HasBasis (uniformity α) (fun x => True) fun n => {p | dist p.fst p.snd < r ^ n}

theorem Metric.uniformity_basis_dist_lt {α : Type u} [PseudoMetricSpace α] {R : ℝ} (hR : 0 < R) : Filter.HasBasis (uniformity α) (fun r => 0 < r ∧ r < R) fun r => {p | dist p.fst p.snd < r}

theorem Metric.mk_uniformity_basis_le {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ} (hf₀ : ∀ (x : β), p x → 0 < f x) (hf : ∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε) : Filter.HasBasis (uniformity α) p fun x => {p | dist p.fst p.snd ≤ f x}

Given f : β → ℝ, if f sends {i | p i} to a set of positive numbers accumulating to zero, then closed neighborhoods of the diagonal of sizes {f i | p i} form a basis of 𝓤 α.

Currently we have only one specific basis uniformity_basis_dist_le based on this constructor. More can be easily added if needed in the future.

theorem Metric.uniformity_basis_dist_le {α : Type u} [PseudoMetricSpace α] : Filter.HasBasis (uniformity α) (fun x => 0 < x) fun ε => {p | dist p.fst p.snd ≤ ε}

Constant size closed neighborhoods of the diagonal form a basis of the uniformity filter.

theorem Metric.uniformity_basis_dist_le_pow {α : Type u} [PseudoMetricSpace α] {r : ℝ} (h0 : 0 < r) (h1 : r < 1) : Filter.HasBasis (uniformity α) (fun x => True) fun n => {p | dist p.fst p.snd ≤ r ^ n}

theorem Metric.mem_uniformity_dist {α : Type u} [PseudoMetricSpace α] {s : Set (α × α)} : s ∈ uniformity α ↔ ∃ ε, ε > 0 ∧ ∀ {a b : α}, dist a b < ε → (a, b) ∈ s

theorem Metric.dist_mem_uniformity {α : Type u} [PseudoMetricSpace α] {ε : ℝ} (ε0 : 0 < ε) : {p | dist p.fst p.snd < ε} ∈ uniformity α

A constant size neighborhood of the diagonal is an entourage.

theorem Metric.uniformContinuous_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : UniformContinuous f ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {a b : α}, dist a b < δ → dist (f a) (f b) < ε

theorem Metric.uniformContinuousOn_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist x y < δ → dist (f x) (f y) < ε

theorem Metric.uniformContinuousOn_iff_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist x y ≤ δ → dist (f x) (f y) ≤ ε

theorem Metric.uniformInducing_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : UniformInducing f ↔ UniformContinuous f ∧ ∀ (δ : ℝ), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

theorem Metric.uniformEmbedding_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : UniformEmbedding f ↔ Function.Injective f ∧ UniformContinuous f ∧ ∀ (δ : ℝ), δ > 0 → ∃ ε, ε > 0 ∧ ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ

theorem Metric.controlled_of_uniformEmbedding {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (h : 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 < δ

If a map between pseudometric spaces is a uniform embedding then the distance between f x and f y is controlled in terms of the distance between x and y.

theorem Metric.totallyBounded_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} : TotallyBounded s ↔ ∀ (ε : ℝ), ε > 0 → ∃ t, Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), Metric.ball y ε

theorem Metric.totallyBounded_of_finite_discretization {α : Type u} [PseudoMetricSpace α] {s : Set α} (H : ∀ (ε : ℝ), ε > 0 → ∃ β x F, ∀ (x y : ↑s), F x = F y → dist ↑x ↑y < ε) : TotallyBounded s

A pseudometric space is totally bounded if one can reconstruct up to any ε>0 any element of the space from finitely many data.

theorem Metric.finite_approx_of_totallyBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : TotallyBounded s) (ε : ℝ) : ε > 0 → ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (y : α) (_ : y ∈ t), Metric.ball y ε

theorem Metric.tendstoUniformlyOnFilter_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] {F : ι → β → α} {f : β → α} {p : Filter ι} {p' : Filter β} : TendstoUniformlyOnFilter F f p p' ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι × β) in p ×ˢ p', dist (f n.snd) (F n.fst n.snd) < ε

Expressing uniform convergence using dist

theorem Metric.tendstoLocallyUniformlyOn_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} : TendstoLocallyUniformlyOn F f p s ↔ ∀ (ε : ℝ), ε > 0 → ∀ (x : β), x ∈ s → ∃ t, t ∈ nhdsWithin x s ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε

Expressing locally uniform convergence on a set using dist.

theorem Metric.tendstoUniformlyOn_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] {F : ι → β → α} {f : β → α} {p : Filter ι} {s : Set β} : TendstoUniformlyOn F f p s ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in p, ∀ (x : β), x ∈ s → dist (f x) (F n x) < ε

Expressing uniform convergence on a set using dist.

theorem Metric.tendstoLocallyUniformly_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] [TopologicalSpace β] {F : ι → β → α} {f : β → α} {p : Filter ι} : TendstoLocallyUniformly F f p ↔ ∀ (ε : ℝ), ε > 0 → ∀ (x : β), ∃ t, t ∈ nhds x ∧ ∀ᶠ (n : ι) in p, ∀ (y : β), y ∈ t → dist (f y) (F n y) < ε

Expressing locally uniform convergence using dist.

theorem Metric.tendstoUniformly_iff {α : Type u} {β : Type v} {ι : Type u_2} [PseudoMetricSpace α] {F : ι → β → α} {f : β → α} {p : Filter ι} : TendstoUniformly F f p ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in p, ∀ (x : β), dist (f x) (F n x) < ε

Expressing uniform convergence using dist.

theorem Metric.cauchy_iff {α : Type u} [PseudoMetricSpace α] {f : Filter α} : Cauchy f ↔ Filter.NeBot f ∧ ∀ (ε : ℝ), ε > 0 → ∃ t, t ∈ f ∧ ∀ (x : α), x ∈ t → ∀ (y : α), y ∈ t → dist x y < ε

theorem Metric.nhds_basis_ball {α : Type u} [PseudoMetricSpace α] {x : α} : Filter.HasBasis (nhds x) (fun x => 0 < x) (Metric.ball x)

theorem Metric.mem_nhds_iff {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} : s ∈ nhds x ↔ ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ s

theorem Metric.eventually_nhds_iff {α : Type u} [PseudoMetricSpace α] {x : α} {p : α → Prop} : (∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε, ε > 0 ∧ (⦃y : α⦄ → dist y x < ε → p y)

theorem Metric.eventually_nhds_iff_ball {α : Type u} [PseudoMetricSpace α] {x : α} {p : α → Prop} : (∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε, ε > 0 ∧ ((y : α) → y ∈ Metric.ball x ε → p y)

theorem Metric.eventually_nhds_prod_iff {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : α × ι → Prop} : (∀ᶠ (x : α × ι) in nhds x₀ ×ˢ f, p x) ↔ ∃ ε, ε > 0 ∧ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ({x : α} → dist x x₀ < ε → {i : ι} → pa i → p (x, i))

A version of Filter.eventually_prod_iff where the first filter consists of neighborhoods in a pseudo-metric space.

theorem Metric.eventually_prod_nhds_iff {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : ι × α → Prop} : (∀ᶠ (x : ι × α) in f ×ˢ nhds x₀, p x) ↔ ∃ pa, (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε, ε > 0 ∧ ({i : ι} → pa i → {x : α} → dist x x₀ < ε → p (i, x))

A version of Filter.eventually_prod_iff where the second filter consists of neighborhoods in a pseudo-metric space.

theorem Metric.nhds_basis_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} : Filter.HasBasis (nhds x) (fun ε => 0 < ε) (Metric.closedBall x)

theorem Metric.nhds_basis_ball_inv_nat_succ {α : Type u} [PseudoMetricSpace α] {x : α} : Filter.HasBasis (nhds x) (fun x => True) fun n => Metric.ball x (1 / (↑n + 1))

theorem Metric.nhds_basis_ball_inv_nat_pos {α : Type u} [PseudoMetricSpace α] {x : α} : Filter.HasBasis (nhds x) (fun n => 0 < n) fun n => Metric.ball x (1 / ↑n)

theorem Metric.nhds_basis_ball_pow {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h0 : 0 < r) (h1 : r < 1) : Filter.HasBasis (nhds x) (fun x => True) fun n => Metric.ball x (r ^ n)

theorem Metric.nhds_basis_closedBall_pow {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h0 : 0 < r) (h1 : r < 1) : Filter.HasBasis (nhds x) (fun x => True) fun n => Metric.closedBall x (r ^ n)

theorem Metric.isOpen_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} : IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ ε, ε > 0 ∧ Metric.ball x ε ⊆ s

theorem Metric.isOpen_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsOpen (Metric.ball x ε)

theorem Metric.ball_mem_nhds {α : Type u} [PseudoMetricSpace α] (x : α) {ε : ℝ} (ε0 : 0 < ε) : Metric.ball x ε ∈ nhds x

theorem Metric.closedBall_mem_nhds {α : Type u} [PseudoMetricSpace α] (x : α) {ε : ℝ} (ε0 : 0 < ε) : Metric.closedBall x ε ∈ nhds x

theorem Metric.closedBall_mem_nhds_of_mem {α : Type u} [PseudoMetricSpace α] {x : α} {c : α} {ε : ℝ} (h : x ∈ Metric.ball c ε) : Metric.closedBall c ε ∈ nhds x

theorem Metric.nhdsWithin_basis_ball {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} : Filter.HasBasis (nhdsWithin x s) (fun ε => 0 < ε) fun ε => Metric.ball x ε ∩ s

theorem Metric.mem_nhdsWithin_iff {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} {t : Set α} : s ∈ nhdsWithin x t ↔ ∃ ε, ε > 0 ∧ Metric.ball x ε ∩ t ⊆ s

theorem Metric.tendsto_nhdsWithin_nhdsWithin {α : Type u} {β : Type v} [PseudoMetricSpace α] {s : Set α} [PseudoMetricSpace β] {t : Set β} {f : α → β} {a : α} {b : β} : Filter.Tendsto f (nhdsWithin a s) (nhdsWithin b t) ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε

theorem Metric.tendsto_nhdsWithin_nhds {α : Type u} {β : Type v} [PseudoMetricSpace α] {s : Set α} [PseudoMetricSpace β] {f : α → β} {a : α} {b : β} : Filter.Tendsto f (nhdsWithin a s) (nhds b) ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, x ∈ s → dist x a < δ → dist (f x) b < ε

theorem Metric.tendsto_nhds_nhds {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {a : α} {b : β} : Filter.Tendsto f (nhds a) (nhds b) ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, dist x a < δ → dist (f x) b < ε

theorem Metric.continuousAt_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {a : α} : ContinuousAt f a ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, dist x a < δ → dist (f x) (f a) < ε

theorem Metric.continuousWithinAt_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {a : α} {s : Set α} : ContinuousWithinAt f s a ↔ ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ {x : α}, x ∈ s → dist x a < δ → dist (f x) (f a) < ε

theorem Metric.continuousOn_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {s : Set α} : ContinuousOn f s ↔ ∀ (b : α), b ∈ s → ∀ (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (a : α), a ∈ s → dist a b < δ → dist (f a) (f b) < ε

theorem Metric.continuous_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} : Continuous f ↔ ∀ (b : α) (ε : ℝ), ε > 0 → ∃ δ, δ > 0 ∧ ∀ (a : α), dist a b < δ → dist (f a) (f b) < ε

theorem Metric.tendsto_nhds {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : Filter β} {u : β → α} {a : α} : Filter.Tendsto u f (nhds a) ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in f, dist (u x) a < ε

theorem Metric.continuousAt_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in nhds b, dist (f x) (f b) < ε

theorem Metric.continuousWithinAt_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} : ContinuousWithinAt f s b ↔ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in nhdsWithin b s, dist (f x) (f b) < ε

theorem Metric.continuousOn_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {s : Set β} : ContinuousOn f s ↔ ∀ (b : β), b ∈ s → ∀ (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in nhdsWithin b s, dist (f x) (f b) < ε

theorem Metric.continuous_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (a : β) (ε : ℝ), ε > 0 → ∀ᶠ (x : β) in nhds a, dist (f x) (f a) < ε

theorem Metric.tendsto_atTop {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} : Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : β), n ≥ N → dist (u n) a < ε

theorem Metric.tendsto_atTop' {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] [NoMaxOrder β] {u : β → α} {a : α} : Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : β), n > N → dist (u n) a < ε

A variant of tendsto_atTop that uses ∃ N, ∀ n > N, ... rather than ∃ N, ∀ n ≥ N, ...

theorem Metric.isOpen_singleton_iff {α : Type u_3} [PseudoMetricSpace α] {x : α} : IsOpen {x} ↔ ∃ ε, ε > 0 ∧ ∀ (y : α), dist y x < ε → y = x

theorem Metric.exists_ball_inter_eq_singleton_of_mem_discrete {α : Type u} [PseudoMetricSpace α] {s : Set α} [DiscreteTopology ↑s] {x : α} (hx : x ∈ s) : ∃ ε, ε > 0 ∧ Metric.ball x ε ∩ s = {x}

Given a point x in a discrete subset s of a pseudometric space, there is an open ball centered at x and intersecting s only at x.

theorem Metric.exists_closedBall_inter_eq_singleton_of_discrete {α : Type u} [PseudoMetricSpace α] {s : Set α} [DiscreteTopology ↑s] {x : α} (hx : x ∈ s) : ∃ ε, ε > 0 ∧ Metric.closedBall x ε ∩ s = {x}

Given a point x in a discrete subset s of a pseudometric space, there is a closed ball of positive radius centered at x and intersecting s only at x.

theorem Dense.exists_dist_lt {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Dense s) (x : α) {ε : ℝ} (hε : 0 < ε) : ∃ y, y ∈ s ∧ dist x y < ε

theorem DenseRange.exists_dist_lt {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {f : β → α} (hf : DenseRange f) (x : α) {ε : ℝ} (hε : 0 < ε) : ∃ y, dist x (f y) < ε

theorem Metric.uniformity_edist_aux {α : Type u_3} (d : α → α → NNReal) : ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | ↑(d p.fst p.snd) < ε} = ⨅ (ε : ENNReal) (_ : ε > 0), Filter.principal {p | ↑(d p.fst p.snd) < ε}

theorem Metric.uniformity_edist {α : Type u} [PseudoMetricSpace α] : uniformity α = ⨅ (ε : ENNReal) (_ : ε > 0), Filter.principal {p | edist p.fst p.snd < ε}

instance PseudoMetricSpace.toPseudoEMetricSpace {α : Type u} [PseudoMetricSpace α] : PseudoEMetricSpace α

A pseudometric space induces a pseudoemetric space

Equations

• One or more equations did not get rendered due to their size.

@[deprecated uniformity_basis_edist]

theorem Metric.uniformity_basis_edist {α : Type u} [PseudoMetricSpace α] : Filter.HasBasis (uniformity α) (fun ε => 0 < ε) fun ε => {p | edist p.fst p.snd < ε}

Expressing the uniformity in terms of edist

theorem Metric.eball_top_eq_univ {α : Type u} [PseudoMetricSpace α] (x : α) : EMetric.ball x ⊤ = Set.univ

In a pseudometric space, an open ball of infinite radius is the whole space

@[simp]

theorem Metric.emetric_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : EMetric.ball x (ENNReal.ofReal ε) = Metric.ball x ε

Balls defined using the distance or the edistance coincide

@[simp]

theorem Metric.emetric_ball_nnreal {α : Type u} [PseudoMetricSpace α] {x : α} {ε : NNReal} : EMetric.ball x ↑ε = Metric.ball x ↑ε

Balls defined using the distance or the edistance coincide

theorem Metric.emetric_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 ≤ ε) : EMetric.closedBall x (ENNReal.ofReal ε) = Metric.closedBall x ε

Closed balls defined using the distance or the edistance coincide

@[simp]

theorem Metric.emetric_closedBall_nnreal {α : Type u} [PseudoMetricSpace α] {x : α} {ε : NNReal} : EMetric.closedBall x ↑ε = Metric.closedBall x ↑ε

Closed balls defined using the distance or the edistance coincide

@[simp]

theorem Metric.emetric_ball_top {α : Type u} [PseudoMetricSpace α] (x : α) : EMetric.ball x ⊤ = Set.univ

theorem Metric.inseparable_iff {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} : Inseparable x y ↔ dist x y = 0

@[reducible]

def PseudoMetricSpace.replaceUniformity {α : Type u_3} [U : UniformSpace α] (m : PseudoMetricSpace α) (H : uniformity α = uniformity α) : PseudoMetricSpace α

Build a new pseudometric space from an old one where the bundled uniform structure is provably (but typically non-definitionaly) equal to some given uniform structure. See Note [forgetful inheritance].

Equations

• One or more equations did not get rendered due to their size.

theorem PseudoMetricSpace.replaceUniformity_eq {α : Type u_3} [U : UniformSpace α] (m : PseudoMetricSpace α) (H : uniformity α = uniformity α) : PseudoMetricSpace.replaceUniformity m H = m

@[reducible]

def PseudoMetricSpace.replaceTopology {γ : Type u_3} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ) (H : U = UniformSpace.toTopologicalSpace) : PseudoMetricSpace γ

Build a new pseudo metric space from an old one where the bundled topological structure is provably (but typically non-definitionaly) equal to some given topological structure. See Note [forgetful inheritance].

Equations

• PseudoMetricSpace.replaceTopology m H = PseudoMetricSpace.replaceUniformity m (_ : uniformity γ = uniformity γ)

theorem PseudoMetricSpace.replaceTopology_eq {γ : Type u_3} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ) (H : U = UniformSpace.toTopologicalSpace) : PseudoMetricSpace.replaceTopology m H = m

def PseudoEMetricSpace.toPseudoMetricSpaceOfDist {α : Type u} [e : PseudoEMetricSpace α] (dist : α → α → ℝ) (edist_ne_top : ∀ (x y : α), edist x y ≠ ⊤) (h : ∀ (x y : α), dist x y = ENNReal.toReal (edist x y)) : PseudoMetricSpace α

One gets a pseudometric 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 pseudometric space and the pseudoemetric 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

• One or more equations did not get rendered due to their size.

@[reducible]

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

One gets a pseudometric 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 pseudometric space and the emetric space.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

def PseudoMetricSpace.replaceBornology {α : Type u_3} [B : Bornology α] (m : PseudoMetricSpace α) (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) : PseudoMetricSpace α

Build a new pseudometric space from an old one where the bundled bornology structure is provably (but typically non-definitionaly) equal to some given bornology structure. See Note [forgetful inheritance].

Equations

• One or more equations did not get rendered due to their size.

theorem PseudoMetricSpace.replaceBornology_eq {α : Type u_3} [m : PseudoMetricSpace α] [B : Bornology α] (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) : PseudoMetricSpace.replaceBornology m H = m

theorem Metric.complete_of_convergent_controlled_sequences {α : Type u} [PseudoMetricSpace α] (B : ℕ → ℝ) (hB : ∀ (n : ℕ), 0 < B n) (H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < B N) → ∃ x, Filter.Tendsto u Filter.atTop (nhds x)) : CompleteSpace α

A very useful criterion to show that a space is complete is to show that all sequences which satisfy a bound of the form dist (u n) (u m) < B N for all n m ≥ N are converging. This is often applied for B N = 2^{-N}, i.e., with a very fast convergence to 0, which makes it possible to use arguments of converging series, while this is impossible to do in general for arbitrary Cauchy sequences.

theorem Metric.complete_of_cauchySeq_tendsto {α : Type u} [PseudoMetricSpace α] : (∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace α

instance Real.pseudoMetricSpace : PseudoMetricSpace ℝ

Instantiate the reals as a pseudometric space.

Equations

• One or more equations did not get rendered due to their size.

theorem Real.dist_eq (x : ℝ) (y : ℝ) : dist x y = |x - y|

theorem Real.nndist_eq (x : ℝ) (y : ℝ) : nndist x y = ↑Real.nnabs (x - y)

theorem Real.nndist_eq' (x : ℝ) (y : ℝ) : nndist x y = ↑Real.nnabs (y - x)

theorem Real.dist_0_eq_abs (x : ℝ) : dist x 0 = |x|

theorem Real.dist_left_le_of_mem_uIcc {x : ℝ} {y : ℝ} {z : ℝ} (h : y ∈ Set.uIcc x z) : dist x y ≤ dist x z

theorem Real.dist_right_le_of_mem_uIcc {x : ℝ} {y : ℝ} {z : ℝ} (h : y ∈ Set.uIcc x z) : dist y z ≤ dist x z

theorem Real.dist_le_of_mem_uIcc {x : ℝ} {y : ℝ} {x' : ℝ} {y' : ℝ} (hx : x ∈ Set.uIcc x' y') (hy : y ∈ Set.uIcc x' y') : dist x y ≤ dist x' y'

theorem Real.dist_le_of_mem_Icc {x : ℝ} {y : ℝ} {x' : ℝ} {y' : ℝ} (hx : x ∈ Set.Icc x' y') (hy : y ∈ Set.Icc x' y') : dist x y ≤ y' - x'

theorem Real.dist_le_of_mem_Icc_01 {x : ℝ} {y : ℝ} (hx : x ∈ Set.Icc 0 1) (hy : y ∈ Set.Icc 0 1) : dist x y ≤ 1

instance instOrderTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstPreorderReal : OrderTopology ℝ

Equations

• instOrderTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstPreorderReal = instOrderTopologyRealToTopologicalSpaceToUniformSpacePseudoMetricSpaceInstPreorderReal.proof_1

theorem Real.ball_eq_Ioo (x : ℝ) (r : ℝ) : Metric.ball x r = Set.Ioo (x - r) (x + r)

theorem Real.closedBall_eq_Icc {x : ℝ} {r : ℝ} : Metric.closedBall x r = Set.Icc (x - r) (x + r)

theorem Real.Ioo_eq_ball (x : ℝ) (y : ℝ) : Set.Ioo x y = Metric.ball ((x + y) / 2) ((y - x) / 2)

theorem Real.Icc_eq_closedBall (x : ℝ) (y : ℝ) : Set.Icc x y = Metric.closedBall ((x + y) / 2) ((y - x) / 2)

theorem totallyBounded_Icc {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : TotallyBounded (Set.Icc a b)

theorem totallyBounded_Ico {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : TotallyBounded (Set.Ico a b)

theorem totallyBounded_Ioc {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : TotallyBounded (Set.Ioc a b)

theorem totallyBounded_Ioo {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : TotallyBounded (Set.Ioo a b)

theorem squeeze_zero' {α : Type u_3} {f : α → ℝ} {g : α → ℝ} {t₀ : Filter α} (hf : ∀ᶠ (t : α) in t₀, 0 ≤ f t) (hft : ∀ᶠ (t : α) in t₀, f t ≤ g t) (g0 : Filter.Tendsto g t₀ (nhds 0)) : Filter.Tendsto f t₀ (nhds 0)

Special case of the sandwich theorem; see tendsto_of_tendsto_of_tendsto_of_le_of_le' for the general case.

theorem squeeze_zero {α : Type u_3} {f : α → ℝ} {g : α → ℝ} {t₀ : Filter α} (hf : ∀ (t : α), 0 ≤ f t) (hft : ∀ (t : α), f t ≤ g t) (g0 : Filter.Tendsto g t₀ (nhds 0)) : Filter.Tendsto f t₀ (nhds 0)

Special case of the sandwich theorem; see tendsto_of_tendsto_of_tendsto_of_le_of_le and tendsto_of_tendsto_of_tendsto_of_le_of_le' for the general case.

theorem Metric.uniformity_eq_comap_nhds_zero {α : Type u} [PseudoMetricSpace α] : uniformity α = Filter.comap (fun p => dist p.fst p.snd) (nhds 0)

theorem cauchySeq_iff_tendsto_dist_atTop_0 {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ Filter.Tendsto (fun n => dist (u n.fst) (u n.snd)) Filter.atTop (nhds 0)

theorem tendsto_uniformity_iff_dist_tendsto_zero {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : ι → α × α} {p : Filter ι} : Filter.Tendsto f p (uniformity α) ↔ Filter.Tendsto (fun x => dist (f x).fst (f x).snd) p (nhds 0)

theorem Filter.Tendsto.congr_dist {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f₁ : ι → α} {f₂ : ι → α} {p : Filter ι} {a : α} (h₁ : Filter.Tendsto f₁ p (nhds a)) (h : Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0)) : Filter.Tendsto f₂ p (nhds a)

theorem tendsto_of_tendsto_of_dist {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f₁ : ι → α} {f₂ : ι → α} {p : Filter ι} {a : α} (h₁ : Filter.Tendsto f₁ p (nhds a)) (h : Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0)) : Filter.Tendsto f₂ p (nhds a)

Alias of Filter.Tendsto.congr_dist.

theorem tendsto_iff_of_dist {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f₁ : ι → α} {f₂ : ι → α} {p : Filter ι} {a : α} (h : Filter.Tendsto (fun x => dist (f₁ x) (f₂ x)) p (nhds 0)) : Filter.Tendsto f₁ p (nhds a) ↔ Filter.Tendsto f₂ p (nhds a)

theorem eventually_closedBall_subset {α : Type u} [PseudoMetricSpace α] {x : α} {u : Set α} (hu : u ∈ nhds x) : ∀ᶠ (r : ℝ) in nhds 0, Metric.closedBall x r ⊆ u

If u is a neighborhood of x, then for small enough r, the closed ball Metric.closedBall x r is contained in u.

theorem Metric.cauchySeq_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → dist (u m) (u n) < ε

In a pseudometric space, Cauchy sequences are characterized by the fact that, eventually, the distance between its elements is arbitrarily small

theorem Metric.cauchySeq_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (n : β), n ≥ N → dist (u n) (u N) < ε

A variation around the pseudometric characterization of Cauchy sequences

theorem Metric.uniformCauchySeqOn_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {γ : Type u_3} {F : β → γ → α} {s : Set γ} : UniformCauchySeqOn F Filter.atTop s ↔ ∀ (ε : ℝ), ε > 0 → ∃ N, ∀ (m : β), m ≥ N → ∀ (n : β), n ≥ N → ∀ (x : γ), x ∈ s → dist (F m x) (F n x) < ε

In a pseudometric space, uniform Cauchy sequences are characterized by the fact that, eventually, the distance between all its elements is uniformly, arbitrarily small

theorem cauchySeq_of_le_tendsto_0' {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {s : β → α} (b : β → ℝ) (h : ∀ (n m : β), n ≤ m → dist (s n) (s m) ≤ b n) (h₀ : Filter.Tendsto b Filter.atTop (nhds 0)) : CauchySeq s

If the distance between s n and s m, n ≤ m is bounded above by b n and b converges to zero, then s is a Cauchy sequence.

theorem cauchySeq_of_le_tendsto_0 {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {s : β → α} (b : β → ℝ) (h : ∀ (n m N : β), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) (h₀ : Filter.Tendsto b Filter.atTop (nhds 0)) : CauchySeq s

If the distance between s n and s m, n, m ≥ N is bounded above by b N and b converges to zero, then s is a Cauchy sequence.

theorem cauchySeq_bdd {α : Type u} [PseudoMetricSpace α] {u : ℕ → α} (hu : CauchySeq u) : ∃ R, R > 0 ∧ ∀ (m n : ℕ), dist (u m) (u n) < R

A Cauchy sequence on the natural numbers is bounded.

theorem cauchySeq_iff_le_tendsto_0 {α : Type u} [PseudoMetricSpace α] {s : ℕ → α} : CauchySeq s ↔ ∃ b, (∀ (n : ℕ), 0 ≤ b n) ∧ (∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Filter.Tendsto b Filter.atTop (nhds 0)

Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.

@[reducible]

def PseudoMetricSpace.induced {α : Type u_3} {β : Type u_4} (f : α → β) (m : PseudoMetricSpace β) : PseudoMetricSpace α

Pseudometric space structure pulled back by a function.

Equations

• One or more equations did not get rendered due to their size.

def Inducing.comapPseudoMetricSpace {α : Type u_3} {β : Type u_4} [TopologicalSpace α] [m : PseudoMetricSpace β] {f : α → β} (hf : Inducing f) : PseudoMetricSpace α

Pull back a pseudometric space structure by an inducing map. This is a version of PseudoMetricSpace.induced useful in case if the domain already has a TopologicalSpace structure.

Equations

• Inducing.comapPseudoMetricSpace hf = PseudoMetricSpace.replaceTopology (PseudoMetricSpace.induced f m) (_ : inst = TopologicalSpace.induced f UniformSpace.toTopologicalSpace)

def UniformInducing.comapPseudoMetricSpace {α : Type u_3} {β : Type u_4} [UniformSpace α] [m : PseudoMetricSpace β] (f : α → β) (h : UniformInducing f) : PseudoMetricSpace α

Pull back a pseudometric space structure by a uniform inducing map. This is a version of PseudoMetricSpace.induced useful in case if the domain already has a UniformSpace structure.

Equations

• UniformInducing.comapPseudoMetricSpace f h = PseudoMetricSpace.replaceUniformity (PseudoMetricSpace.induced f m) (_ : uniformity α = Filter.comap (fun x => (f x.fst, f x.snd)) (uniformity β))

instance Subtype.pseudoMetricSpace {α : Type u} [PseudoMetricSpace α] {p : α → Prop} : PseudoMetricSpace (Subtype p)

Equations

• Subtype.pseudoMetricSpace = PseudoMetricSpace.induced Subtype.val inst

theorem Subtype.dist_eq {α : Type u} [PseudoMetricSpace α] {p : α → Prop} (x : Subtype p) (y : Subtype p) : dist x y = dist ↑x ↑y

theorem Subtype.nndist_eq {α : Type u} [PseudoMetricSpace α] {p : α → Prop} (x : Subtype p) (y : Subtype p) : nndist x y = nndist ↑x ↑y

instance AddOpposite.instPseudoMetricSpaceAddOpposite {α : Type u} [PseudoMetricSpace α] : PseudoMetricSpace αᵃᵒᵖ

Equations

• AddOpposite.instPseudoMetricSpaceAddOpposite = PseudoMetricSpace.induced AddOpposite.unop inst

instance MulOpposite.instPseudoMetricSpaceMulOpposite {α : Type u} [PseudoMetricSpace α] : PseudoMetricSpace αᵐᵒᵖ

Equations

• MulOpposite.instPseudoMetricSpaceMulOpposite = PseudoMetricSpace.induced MulOpposite.unop inst

@[simp]

theorem AddOpposite.dist_unop {α : Type u} [PseudoMetricSpace α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) : dist (AddOpposite.unop x) (AddOpposite.unop y) = dist x y

@[simp]

theorem MulOpposite.dist_unop {α : Type u} [PseudoMetricSpace α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) : dist (MulOpposite.unop x) (MulOpposite.unop y) = dist x y

@[simp]

theorem AddOpposite.dist_op {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : dist (AddOpposite.op x) (AddOpposite.op y) = dist x y

@[simp]

theorem MulOpposite.dist_op {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : dist (MulOpposite.op x) (MulOpposite.op y) = dist x y

@[simp]

theorem AddOpposite.nndist_unop {α : Type u} [PseudoMetricSpace α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) : nndist (AddOpposite.unop x) (AddOpposite.unop y) = nndist x y

@[simp]

theorem MulOpposite.nndist_unop {α : Type u} [PseudoMetricSpace α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) : nndist (MulOpposite.unop x) (MulOpposite.unop y) = nndist x y

@[simp]

theorem AddOpposite.nndist_op {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : nndist (AddOpposite.op x) (AddOpposite.op y) = nndist x y

@[simp]

theorem MulOpposite.nndist_op {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) : nndist (MulOpposite.op x) (MulOpposite.op y) = nndist x y

instance instPseudoMetricSpaceNNReal : PseudoMetricSpace NNReal

Equations

• instPseudoMetricSpaceNNReal = Subtype.pseudoMetricSpace

theorem NNReal.dist_eq (a : NNReal) (b : NNReal) : dist a b = |↑a - ↑b|

theorem NNReal.nndist_eq (a : NNReal) (b : NNReal) : nndist a b = max (a - b) (b - a)

@[simp]

theorem NNReal.nndist_zero_eq_val (z : NNReal) : nndist 0 z = z

@[simp]

theorem NNReal.nndist_zero_eq_val' (z : NNReal) : nndist z 0 = z

theorem NNReal.le_add_nndist (a : NNReal) (b : NNReal) : a ≤ b + nndist a b

instance instPseudoMetricSpaceULift {β : Type v} [PseudoMetricSpace β] : PseudoMetricSpace (ULift.{u_3, v} β)

Equations

• instPseudoMetricSpaceULift = PseudoMetricSpace.induced ULift.down inst

theorem ULift.dist_eq {β : Type v} [PseudoMetricSpace β] (x : ULift.{u_3, v} β) (y : ULift.{u_3, v} β) : dist x y = dist x.down y.down

theorem ULift.nndist_eq {β : Type v} [PseudoMetricSpace β] (x : ULift.{u_3, v} β) (y : ULift.{u_3, v} β) : nndist x y = nndist x.down y.down

@[simp]

theorem ULift.dist_up_up {β : Type v} [PseudoMetricSpace β] (x : β) (y : β) : dist { down := x } { down := y } = dist x y

@[simp]

theorem ULift.nndist_up_up {β : Type v} [PseudoMetricSpace β] (x : β) (y : β) : nndist { down := x } { down := y } = nndist x y

instance Prod.pseudoMetricSpaceMax {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] : PseudoMetricSpace (α × β)

Equations

• One or more equations did not get rendered due to their size.

theorem Prod.dist_eq {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {x : α × β} {y : α × β} : dist x y = max (dist x.fst y.fst) (dist x.snd y.snd)

@[simp]

theorem dist_prod_same_left {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {x : α} {y₁ : β} {y₂ : β} : dist (x, y₁) (x, y₂) = dist y₁ y₂

@[simp]

theorem dist_prod_same_right {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {x₁ : α} {x₂ : α} {y : β} : dist (x₁, y) (x₂, y) = dist x₁ x₂

theorem ball_prod_same {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α) (y : β) (r : ℝ) : Metric.ball x r ×ˢ Metric.ball y r = Metric.ball (x, y) r

theorem closedBall_prod_same {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α) (y : β) (r : ℝ) : Metric.closedBall x r ×ˢ Metric.closedBall y r = Metric.closedBall (x, y) r

theorem sphere_prod {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] (x : α × β) (r : ℝ) : Metric.sphere x r = Metric.sphere x.fst r ×ˢ Metric.closedBall x.snd r ∪ Metric.closedBall x.fst r ×ˢ Metric.sphere x.snd r

theorem dist_dist_dist_le_left {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) : dist (dist x z) (dist y z) ≤ dist x y

theorem dist_dist_dist_le_right {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (z : α) : dist (dist x y) (dist x z) ≤ dist y z

theorem dist_dist_dist_le {α : Type u} [PseudoMetricSpace α] (x : α) (y : α) (x' : α) (y' : α) : dist (dist x y) (dist x' y') ≤ dist x x' + dist y y'

theorem uniformContinuous_dist {α : Type u} [PseudoMetricSpace α] : UniformContinuous fun p => dist p.fst p.snd

theorem UniformContinuous.dist {α : Type u} {β : Type v} [PseudoMetricSpace α] [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun b => dist (f b) (g b)

theorem continuous_dist {α : Type u} [PseudoMetricSpace α] : Continuous fun p => dist p.fst p.snd

theorem Continuous.dist {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {g : β → α} (hf : Continuous f) (hg : Continuous g) : Continuous fun b => dist (f b) (g b)

theorem Filter.Tendsto.dist {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {g : β → α} {x : Filter β} {a : α} {b : α} (hf : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) : Filter.Tendsto (fun x => dist (f x) (g x)) x (nhds (dist a b))

theorem nhds_comap_dist {α : Type u} [PseudoMetricSpace α] (a : α) : Filter.comap (fun x => dist x a) (nhds 0) = nhds a

theorem tendsto_iff_dist_tendsto_zero {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {x : Filter β} {a : α} : Filter.Tendsto f x (nhds a) ↔ Filter.Tendsto (fun b => dist (f b) a) x (nhds 0)

theorem continuous_iff_continuous_dist {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} : Continuous f ↔ Continuous fun x => dist (f x.fst) (f x.snd)

theorem uniformContinuous_nndist {α : Type u} [PseudoMetricSpace α] : UniformContinuous fun p => nndist p.fst p.snd

theorem UniformContinuous.nndist {α : Type u} {β : Type v} [PseudoMetricSpace α] [UniformSpace β] {f : β → α} {g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun b => nndist (f b) (g b)

theorem continuous_nndist {α : Type u} [PseudoMetricSpace α] : Continuous fun p => nndist p.fst p.snd

theorem Continuous.nndist {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {g : β → α} (hf : Continuous f) (hg : Continuous g) : Continuous fun b => nndist (f b) (g b)

theorem Filter.Tendsto.nndist {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {g : β → α} {x : Filter β} {a : α} {b : α} (hf : Filter.Tendsto f x (nhds a)) (hg : Filter.Tendsto g x (nhds b)) : Filter.Tendsto (fun x => nndist (f x) (g x)) x (nhds (nndist a b))

theorem Metric.isClosed_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsClosed (Metric.closedBall x ε)

theorem Metric.isClosed_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsClosed (Metric.sphere x ε)

@[simp]

theorem Metric.closure_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : closure (Metric.closedBall x ε) = Metric.closedBall x ε

@[simp]

theorem Metric.closure_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : closure (Metric.sphere x ε) = Metric.sphere x ε

theorem Metric.closure_ball_subset_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : closure (Metric.ball x ε) ⊆ Metric.closedBall x ε

theorem Metric.frontier_ball_subset_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : frontier (Metric.ball x ε) ⊆ Metric.sphere x ε

theorem Metric.frontier_closedBall_subset_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : frontier (Metric.closedBall x ε) ⊆ Metric.sphere x ε

theorem Metric.ball_subset_interior_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} : Metric.ball x ε ⊆ interior (Metric.closedBall x ε)

theorem Metric.mem_closure_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} {a : α} : a ∈ closure s ↔ ∀ (ε : ℝ), ε > 0 → ∃ b, b ∈ s ∧ dist a b < ε

ε-characterization of the closure in pseudometric spaces

theorem Metric.mem_closure_range_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {e : β → α} {a : α} : a ∈ closure (Set.range e) ↔ ∀ (ε : ℝ), ε > 0 → ∃ k, dist a (e k) < ε

theorem Metric.mem_closure_range_iff_nat {α : Type u} {β : Type v} [PseudoMetricSpace α] {e : β → α} {a : α} : a ∈ closure (Set.range e) ↔ ∀ (n : ℕ), ∃ k, dist a (e k) < 1 / (↑n + 1)

theorem Metric.mem_of_closed' {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsClosed s) {a : α} : a ∈ s ↔ ∀ (ε : ℝ), ε > 0 → ∃ b, b ∈ s ∧ dist a b < ε

theorem Metric.closedBall_zero' {α : Type u} [PseudoMetricSpace α] (x : α) : Metric.closedBall x 0 = closure {x}

theorem Metric.eventually_isCompact_closedBall {α : Type u} [PseudoMetricSpace α] [LocallyCompactSpace α] (x : α) : ∀ᶠ (r : ℝ) in nhds 0, IsCompact (Metric.closedBall x r)

theorem Metric.exists_isCompact_closedBall {α : Type u} [PseudoMetricSpace α] [LocallyCompactSpace α] (x : α) : ∃ r, 0 < r ∧ IsCompact (Metric.closedBall x r)

theorem Metric.dense_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} : Dense s ↔ ∀ (x : α) (r : ℝ), r > 0 → Set.Nonempty (Metric.ball x r ∩ s)

theorem Metric.denseRange_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} : DenseRange f ↔ ∀ (x : α) (r : ℝ), r > 0 → ∃ y, dist x (f y) < r

theorem Inducing.isSeparable_preimage {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} [TopologicalSpace β] (hf : Inducing f) {s : Set α} (hs : TopologicalSpace.IsSeparable s) : TopologicalSpace.IsSeparable (f ⁻¹' s)

The preimage of a separable set by an inducing map is separable.

theorem Embedding.isSeparable_preimage {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} [TopologicalSpace β] (hf : Embedding f) {s : Set α} (hs : TopologicalSpace.IsSeparable s) : TopologicalSpace.IsSeparable (f ⁻¹' s)

theorem ContinuousOn.isSeparable_image {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : α → β} {s : Set α} (hf : ContinuousOn f s) (hs : TopologicalSpace.IsSeparable s) : TopologicalSpace.IsSeparable (f '' s)

If a map is continuous on a separable set s, then the image of s is also separable.

instance pseudoMetricSpacePi {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] : PseudoMetricSpace ((b : β) → π b)

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

Equations

• One or more equations did not get rendered due to their size.

theorem nndist_pi_def {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) : nndist f g = Finset.sup Finset.univ fun b => nndist (f b) (g b)

theorem dist_pi_def {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) : dist f g = ↑(Finset.sup Finset.univ fun b => nndist (f b) (g b))

theorem nndist_pi_le_iff {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : NNReal} : nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r

theorem nndist_pi_lt_iff {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : NNReal} (hr : 0 < r) : nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r

theorem nndist_pi_eq_iff {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : NNReal} (hr : 0 < r) : nndist f g = r ↔ (∃ i, nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

theorem dist_pi_lt_iff {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : ℝ} (hr : 0 < r) : dist f g < r ↔ ∀ (b : β), dist (f b) (g b) < r

theorem dist_pi_le_iff {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : ℝ} (hr : 0 ≤ r) : dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

theorem dist_pi_eq_iff {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {r : ℝ} (hr : 0 < r) : dist f g = r ↔ (∃ i, dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r

theorem dist_pi_le_iff' {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] [Nonempty β] {f : (b : β) → π b} {g : (b : β) → π b} {r : ℝ} : dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

theorem dist_pi_const_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [Fintype β] (a : α) (b : α) : (dist (fun x => a) fun x => b) ≤ dist a b

theorem nndist_pi_const_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [Fintype β] (a : α) (b : α) : (nndist (fun x => a) fun x => b) ≤ nndist a b

@[simp]

theorem dist_pi_const {α : Type u} {β : Type v} [PseudoMetricSpace α] [Fintype β] [Nonempty β] (a : α) (b : α) : (dist (fun x => a) fun x => b) = dist a b

@[simp]

theorem nndist_pi_const {α : Type u} {β : Type v} [PseudoMetricSpace α] [Fintype β] [Nonempty β] (a : α) (b : α) : (nndist (fun x => a) fun x => b) = nndist a b

theorem nndist_le_pi_nndist {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) (b : β) : nndist (f b) (g b) ≤ nndist f g

theorem dist_le_pi_dist {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (f : (b : β) → π b) (g : (b : β) → π b) (b : β) : dist (f b) (g b) ≤ dist f g

theorem ball_pi {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : ℝ} (hr : 0 < r) : Metric.ball x r = Set.pi Set.univ fun b => Metric.ball (x b) r

An open ball in a product space is a product of open balls. See also ball_pi' for a version assuming Nonempty β instead of 0 < r.

theorem ball_pi' {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] [Nonempty β] (x : (b : β) → π b) (r : ℝ) : Metric.ball x r = Set.pi Set.univ fun b => Metric.ball (x b) r

An open ball in a product space is a product of open balls. See also ball_pi for a version assuming 0 < r instead of Nonempty β.

theorem closedBall_pi {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : ℝ} (hr : 0 ≤ r) : Metric.closedBall x r = Set.pi Set.univ fun b => Metric.closedBall (x b) r

A closed ball in a product space is a product of closed balls. See also closedBall_pi' for a version assuming Nonempty β instead of 0 ≤ r.

theorem closedBall_pi' {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] [Nonempty β] (x : (b : β) → π b) (r : ℝ) : Metric.closedBall x r = Set.pi Set.univ fun b => Metric.closedBall (x b) r

A closed ball in a product space is a product of closed balls. See also closedBall_pi for a version assuming 0 ≤ r instead of Nonempty β.

theorem sphere_pi {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] (x : (b : β) → π b) {r : ℝ} (h : 0 < r ∨ Nonempty β) : Metric.sphere x r = (⋃ (i : β), Function.eval i ⁻¹' Metric.sphere (x i) r) ∩ Metric.closedBall x r

A sphere in a product space is a union of spheres on each component restricted to the closed ball.

@[simp]

theorem Fin.nndist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type u_4} [(i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x : α i) (y : α i) (f : (j : Fin n) → α (Fin.succAbove i j)) (g : (j : Fin n) → α (Fin.succAbove i j)) : nndist (Fin.insertNth i x f) (Fin.insertNth i y g) = max (nndist x y) (nndist f g)

@[simp]

theorem Fin.dist_insertNth_insertNth {n : ℕ} {α : Fin (n + 1) → Type u_4} [(i : Fin (n + 1)) → PseudoMetricSpace (α i)] (i : Fin (n + 1)) (x : α i) (y : α i) (f : (j : Fin n) → α (Fin.succAbove i j)) (g : (j : Fin n) → α (Fin.succAbove i j)) : dist (Fin.insertNth i x f) (Fin.insertNth i y g) = max (dist x y) (dist f g)

theorem Real.dist_le_of_mem_pi_Icc {β : Type v} [Fintype β] {x : β → ℝ} {y : β → ℝ} {x' : β → ℝ} {y' : β → ℝ} (hx : x ∈ Set.Icc x' y') (hy : y ∈ Set.Icc x' y') : dist x y ≤ dist x' y'

theorem finite_cover_balls_of_compact {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) {e : ℝ} (he : 0 < e) : ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), Metric.ball x e

Any compact set in a pseudometric space can be covered by finitely many balls of a given positive radius

theorem IsCompact.finite_cover_balls {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) {e : ℝ} (he : 0 < e) : ∃ t, t ⊆ s ∧ Set.Finite t ∧ s ⊆ ⋃ (x : α) (_ : x ∈ t), Metric.ball x e

Alias of finite_cover_balls_of_compact.

---

Any compact set in a pseudometric space can be covered by finitely many balls of a given positive radius

class ProperSpace (α : Type u) [PseudoMetricSpace α] : Prop

• isCompact_closedBall : ∀ (x : α) (r : ℝ), IsCompact (Metric.closedBall x r)

A pseudometric space is proper if all closed balls are compact.

theorem isCompact_sphere {α : Type u_3} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : IsCompact (Metric.sphere x r)

In a proper pseudometric space, all spheres are compact.

instance Metric.sphere.compactSpace {α : Type u_3} [PseudoMetricSpace α] [ProperSpace α] (x : α) (r : ℝ) : CompactSpace ↑(Metric.sphere x r)

In a proper pseudometric space, any sphere is a CompactSpace when considered as a subtype.

Equations

• @Metric.sphere.compactSpace = @Metric.sphere.compactSpace.proof_1

instance secondCountable_of_proper {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : TopologicalSpace.SecondCountableTopology α

A proper pseudo metric space is sigma compact, and therefore second countable.

Equations

• @secondCountable_of_proper = @secondCountable_of_proper.proof_1

theorem tendsto_dist_right_cocompact_atTop {α : Type u} [PseudoMetricSpace α] [ProperSpace α] (x : α) : Filter.Tendsto (fun y => dist y x) (Filter.cocompact α) Filter.atTop

theorem tendsto_dist_left_cocompact_atTop {α : Type u} [PseudoMetricSpace α] [ProperSpace α] (x : α) : Filter.Tendsto (dist x) (Filter.cocompact α) Filter.atTop

theorem properSpace_of_compact_closedBall_of_le {α : Type u} [PseudoMetricSpace α] (R : ℝ) (h : ∀ (x : α) (r : ℝ), R ≤ r → IsCompact (Metric.closedBall x r)) : ProperSpace α

If all closed balls of large enough radius are compact, then the space is proper. Especially useful when the lower bound for the radius is 0.

instance proper_of_compact {α : Type u} [PseudoMetricSpace α] [CompactSpace α] : ProperSpace α

Equations

• @proper_of_compact = @proper_of_compact.proof_1

instance locally_compact_of_proper {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : LocallyCompactSpace α

A proper space is locally compact

Equations

• @locally_compact_of_proper = @locally_compact_of_proper.proof_1

instance complete_of_proper {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : CompleteSpace α

A proper space is complete

Equations

• @complete_of_proper = @complete_of_proper.proof_1

instance prod_properSpace {α : Type u_3} {β : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [ProperSpace α] [ProperSpace β] : ProperSpace (α × β)

A binary product of proper spaces is proper.

Equations

• @prod_properSpace = @prod_properSpace.proof_1

instance pi_properSpace {β : Type v} {π : β → Type u_3} [Fintype β] [(b : β) → PseudoMetricSpace (π b)] [h : ∀ (b : β), ProperSpace (π b)] : ProperSpace ((b : β) → π b)

A finite product of proper spaces is proper.

Equations

• @pi_properSpace = @pi_properSpace.proof_1

theorem exists_pos_lt_subset_ball {α : Type u} [PseudoMetricSpace α] [ProperSpace α] {x : α} {r : ℝ} {s : Set α} (hr : 0 < r) (hs : IsClosed s) (h : s ⊆ Metric.ball x r) : ∃ r', r' ∈ Set.Ioo 0 r ∧ s ⊆ Metric.ball x r'

If a nonempty ball in a proper space includes a closed set s, then there exists a nonempty ball with the same center and a strictly smaller radius that includes s.

theorem exists_lt_subset_ball {α : Type u} [PseudoMetricSpace α] [ProperSpace α] {x : α} {r : ℝ} {s : Set α} (hs : IsClosed s) (h : s ⊆ Metric.ball x r) : ∃ r', r' < r ∧ s ⊆ Metric.ball x r'

If a ball in a proper space includes a closed set s, then there exists a ball with the same center and a strictly smaller radius that includes s.

theorem IsCompact.isSeparable {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) : TopologicalSpace.IsSeparable s

theorem Metric.secondCountable_of_almost_dense_set {α : Type u} [PseudoMetricSpace α] (H : ∀ (ε : ℝ), ε > 0 → ∃ s, Set.Countable s ∧ ∀ (x : α), ∃ y, y ∈ s ∧ dist x y ≤ ε) : TopologicalSpace.SecondCountableTopology α

A pseudometric space is second countable if, for every ε > 0, there is a countable set which is ε-dense.

theorem lebesgue_number_lemma_of_metric {α : Type u} [PseudoMetricSpace α] {s : Set α} {ι : Sort u_3} {c : ι → Set α} (hs : IsCompact s) (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : s ⊆ ⋃ (i : ι), c i) : ∃ δ, δ > 0 ∧ ∀ (x : α), x ∈ s → ∃ i, Metric.ball x δ ⊆ c i

theorem lebesgue_number_lemma_of_metric_sUnion {α : Type u} [PseudoMetricSpace α] {s : Set α} {c : Set (Set α)} (hs : IsCompact s) (hc₁ : ∀ (t : Set α), t ∈ c → IsOpen t) (hc₂ : s ⊆ ⋃₀ c) : ∃ δ, δ > 0 ∧ ∀ (x : α), x ∈ s → ∃ t, t ∈ c ∧ Metric.ball x δ ⊆ t

theorem Metric.isBounded_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} : Bornology.IsBounded (Metric.closedBall x r)

Closed balls are bounded

theorem Metric.isBounded_ball {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} : Bornology.IsBounded (Metric.ball x r)

Open balls are bounded

theorem Metric.isBounded_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} : Bornology.IsBounded (Metric.sphere x r)

Spheres are bounded

theorem Metric.isBounded_iff_subset_closedBall {α : Type u} [PseudoMetricSpace α] {s : Set α} (c : α) : Bornology.IsBounded s ↔ ∃ r, s ⊆ Metric.closedBall c r

Given a point, a bounded subset is included in some ball around this point

theorem Bornology.IsBounded.subset_closedBall {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (c : α) : ∃ r, s ⊆ Metric.closedBall c r

theorem Bornology.IsBounded.subset_ball_lt {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (a : ℝ) (c : α) : ∃ r, a < r ∧ s ⊆ Metric.ball c r

theorem Bornology.IsBounded.subset_ball {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (c : α) : ∃ r, s ⊆ Metric.ball c r

theorem Bornology.IsBounded.subset_closedBall_lt {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) (a : ℝ) (c : α) : ∃ r, a < r ∧ s ⊆ Metric.closedBall c r

theorem Metric.isBounded_closure_of_isBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) : Bornology.IsBounded (closure s)

theorem Bornology.IsBounded.closure {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : Bornology.IsBounded s) : Bornology.IsBounded (closure s)

@[simp]

theorem Metric.isBounded_closure_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded (closure s) ↔ Bornology.IsBounded s

theorem TotallyBounded.isBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : TotallyBounded s) : Bornology.IsBounded s

A totally bounded set is bounded

theorem IsCompact.isBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : IsCompact s) : Bornology.IsBounded s

A compact set is bounded

theorem Metric.isBounded_range_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} : Bornology.IsBounded (Set.range f) ↔ ∃ C, ∀ (x y : β), dist (f x) (f y) ≤ C

Characterization of the boundedness of the range of a function

theorem Metric.isBounded_image_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {s : Set β} : Bornology.IsBounded (f '' s) ↔ ∃ C, ∀ (x : β), x ∈ s → ∀ (y : β), y ∈ s → dist (f x) (f y) ≤ C

theorem Metric.isBounded_range_of_tendsto_cofinite_uniformity {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} (hf : Filter.Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (uniformity α)) : Bornology.IsBounded (Set.range f)

theorem Metric.isBounded_range_of_cauchy_map_cofinite {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} (hf : Cauchy (Filter.map f Filter.cofinite)) : Bornology.IsBounded (Set.range f)

theorem CauchySeq.isBounded_range {α : Type u} [PseudoMetricSpace α] {f : ℕ → α} (hf : CauchySeq f) : Bornology.IsBounded (Set.range f)

theorem Metric.isBounded_range_of_tendsto_cofinite {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {a : α} (hf : Filter.Tendsto f Filter.cofinite (nhds a)) : Bornology.IsBounded (Set.range f)

theorem Metric.isBounded_of_compactSpace {α : Type u} [PseudoMetricSpace α] {s : Set α} [CompactSpace α] : Bornology.IsBounded s

In a compact space, all sets are bounded

theorem Metric.isBounded_range_of_tendsto {α : Type u} [PseudoMetricSpace α] (u : ℕ → α) {x : α} (hu : Filter.Tendsto u Filter.atTop (nhds x)) : Bornology.IsBounded (Set.range u)

theorem Metric.disjoint_nhds_cobounded {α : Type u} [PseudoMetricSpace α] (x : α) : Disjoint (nhds x) (Bornology.cobounded α)

theorem Metric.disjoint_cobounded_nhds {α : Type u} [PseudoMetricSpace α] (x : α) : Disjoint (Bornology.cobounded α) (nhds x)

theorem Metric.disjoint_nhdsSet_cobounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) : Disjoint (nhdsSet s) (Bornology.cobounded α)

theorem Metric.disjoint_cobounded_nhdsSet {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsCompact s) : Disjoint (Bornology.cobounded α) (nhdsSet s)

theorem Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_forall_continuousWithinAt {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {s : Set β} {f : β → α} (hk : IsCompact k) (hf : ∀ (x : β), x ∈ k → ContinuousWithinAt f s x) : ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))

If a function is continuous within a set s at every point of a compact set k, then it is bounded on some open neighborhood of k in s.

theorem Metric.exists_isOpen_isBounded_image_of_isCompact_of_forall_continuousAt {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {f : β → α} (hk : IsCompact k) (hf : ∀ (x : β), x ∈ k → ContinuousAt f x) : ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)

If a function is continuous at every point of a compact set k, then it is bounded on some open neighborhood of k.

theorem Metric.exists_isOpen_isBounded_image_inter_of_isCompact_of_continuousOn {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {s : Set β} {f : β → α} (hk : IsCompact k) (hks : k ⊆ s) (hf : ContinuousOn f s) : ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' (t ∩ s))

If a function is continuous on a set s containing a compact set k, then it is bounded on some open neighborhood of k in s.

theorem Metric.exists_isOpen_isBounded_image_of_isCompact_of_continuousOn {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {k : Set β} {s : Set β} {f : β → α} (hk : IsCompact k) (hs : IsOpen s) (hks : k ⊆ s) (hf : ContinuousOn f s) : ∃ t, k ⊆ t ∧ IsOpen t ∧ Bornology.IsBounded (f '' t)

If a function is continuous on a neighborhood of a compact set k, then it is bounded on some open neighborhood of k.

theorem Metric.isCompact_of_isClosed_isBounded {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (hc : IsClosed s) (hb : Bornology.IsBounded s) : IsCompact s

The Heine–Borel theorem: In a proper space, a closed bounded set is compact.

theorem Bornology.IsBounded.isCompact_closure {α : Type u} [PseudoMetricSpace α] {s : Set α} [ProperSpace α] (h : Bornology.IsBounded s) : IsCompact (closure s)

The Heine–Borel theorem: In a proper space, the closure of a bounded set is compact.

theorem Metric.isCompact_iff_isClosed_bounded {α : Type u} [PseudoMetricSpace α] {s : Set α} [T2Space α] [ProperSpace α] : IsCompact s ↔ IsClosed s ∧ Bornology.IsBounded s

The Heine–Borel theorem: In a proper Hausdorff space, a set is compact if and only if it is closed and bounded.

theorem Metric.compactSpace_iff_isBounded_univ {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : CompactSpace α ↔ Bornology.IsBounded Set.univ

theorem Metric.isBounded_Icc {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : Bornology.IsBounded (Set.Icc a b)

theorem Metric.isBounded_Ico {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : Bornology.IsBounded (Set.Ico a b)

theorem Metric.isBounded_Ioc {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : Bornology.IsBounded (Set.Ioc a b)

theorem Metric.isBounded_Ioo {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] (a : α) (b : α) : Bornology.IsBounded (Set.Ioo a b)

theorem Metric.isBounded_of_bddAbove_of_bddBelow {α : Type u} [PseudoMetricSpace α] [Preorder α] [CompactIccSpace α] {s : Set α} (h₁ : BddAbove s) (h₂ : BddBelow s) : Bornology.IsBounded s

In a pseudo metric space with a conditionally complete linear order such that the order and the metric structure give the same topology, any order-bounded set is metric-bounded.

noncomputable def Metric.diam {α : Type u} [PseudoMetricSpace α] (s : Set α) : ℝ

The diameter of a set in a metric space. To get controllable behavior even when the diameter should be infinite, we express it in terms of the emetric.diameter

Equations

• Metric.diam s = ENNReal.toReal (EMetric.diam s)

theorem Metric.diam_nonneg {α : Type u} [PseudoMetricSpace α] {s : Set α} : 0 ≤ Metric.diam s

The diameter of a set is always nonnegative

theorem Metric.diam_subsingleton {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Set.Subsingleton s) : Metric.diam s = 0

@[simp]

theorem Metric.diam_empty {α : Type u} [PseudoMetricSpace α] : Metric.diam ∅ = 0

The empty set has zero diameter

@[simp]

theorem Metric.diam_singleton {α : Type u} [PseudoMetricSpace α] {x : α} : Metric.diam {x} = 0

A singleton has zero diameter

theorem Metric.diam_pair {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} : Metric.diam {x, y} = dist x y

theorem Metric.diam_triple {α : Type u} [PseudoMetricSpace α] {x : α} {y : α} {z : α} : Metric.diam {x, y, z} = max (max (dist x y) (dist x z)) (dist y z)

theorem Metric.ediam_le_of_forall_dist_le {α : Type u} [PseudoMetricSpace α] {s : Set α} {C : ℝ} (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist x y ≤ C) : EMetric.diam s ≤ ENNReal.ofReal C

If the distance between any two points in a set is bounded by some constant C, then ENNReal.ofReal C bounds the emetric diameter of this set.

theorem Metric.diam_le_of_forall_dist_le {α : Type u} [PseudoMetricSpace α] {s : Set α} {C : ℝ} (h₀ : 0 ≤ C) (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist x y ≤ C) : Metric.diam s ≤ C

If the distance between any two points in a set is bounded by some non-negative constant, this constant bounds the diameter.

theorem Metric.diam_le_of_forall_dist_le_of_nonempty {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Set.Nonempty s) {C : ℝ} (h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist x y ≤ C) : Metric.diam s ≤ C

If the distance between any two points in a nonempty set is bounded by some constant, this constant bounds the diameter.

theorem Metric.dist_le_diam_of_mem' {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} (h : EMetric.diam s ≠ ⊤) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ Metric.diam s

The distance between two points in a set is controlled by the diameter of the set.

theorem Metric.isBounded_iff_ediam_ne_top {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded s ↔ EMetric.diam s ≠ ⊤

Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.

theorem Bornology.IsBounded.ediam_ne_top {α : Type u} [PseudoMetricSpace α] {s : Set α} : Bornology.IsBounded s → EMetric.diam s ≠ ⊤

Alias of the forward direction of Metric.isBounded_iff_ediam_ne_top.

---

Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.

theorem Metric.ediam_eq_top_iff_unbounded {α : Type u} [PseudoMetricSpace α] {s : Set α} : EMetric.diam s = ⊤ ↔ ¬Bornology.IsBounded s

theorem Metric.ediam_univ_eq_top_iff_noncompact {α : Type u} [PseudoMetricSpace α] [ProperSpace α] : EMetric.diam Set.univ = ⊤ ↔ NoncompactSpace α

@[simp]

theorem Metric.ediam_univ_of_noncompact {α : Type u} [PseudoMetricSpace α] [ProperSpace α] [NoncompactSpace α] : EMetric.diam Set.univ = ⊤

@[simp]

theorem Metric.diam_univ_of_noncompact {α : Type u} [PseudoMetricSpace α] [ProperSpace α] [NoncompactSpace α] : Metric.diam Set.univ = 0

theorem Metric.dist_le_diam_of_mem {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} (h : Bornology.IsBounded s) (hx : x ∈ s) (hy : y ∈ s) : dist x y ≤ Metric.diam s

The distance between two points in a set is controlled by the diameter of the set.

theorem Metric.ediam_of_unbounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : ¬Bornology.IsBounded s) : EMetric.diam s = ⊤

theorem Metric.diam_eq_zero_of_unbounded {α : Type u} [PseudoMetricSpace α] {s : Set α} (h : ¬Bornology.IsBounded s) : Metric.diam s = 0

An unbounded set has zero diameter. If you would prefer to get the value ∞, use EMetric.diam. This lemma makes it possible to avoid side conditions in some situations

theorem Metric.diam_mono {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} (h : s ⊆ t) (ht : Bornology.IsBounded t) : Metric.diam s ≤ Metric.diam t

If s ⊆ t, then the diameter of s is bounded by that of t, provided t is bounded.

theorem Metric.diam_union {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {y : α} {t : Set α} (xs : x ∈ s) (yt : y ∈ t) : Metric.diam (s ∪ t) ≤ Metric.diam s + dist x y + Metric.diam t

The diameter of a union is controlled by the sum of the diameters, and the distance between any two points in each of the sets. This lemma is true without any side condition, since it is obviously true if s ∪ t is unbounded.

theorem Metric.diam_union' {α : Type u} [PseudoMetricSpace α] {s : Set α} {t : Set α} (h : Set.Nonempty (s ∩ t)) : Metric.diam (s ∪ t) ≤ Metric.diam s + Metric.diam t

If two sets intersect, the diameter of the union is bounded by the sum of the diameters.

theorem Metric.diam_le_of_subset_closedBall {α : Type u} [PseudoMetricSpace α] {s : Set α} {x : α} {r : ℝ} (hr : 0 ≤ r) (h : s ⊆ Metric.closedBall x r) : Metric.diam s ≤ 2 * r

theorem Metric.diam_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h : 0 ≤ r) : Metric.diam (Metric.closedBall x r) ≤ 2 * r

The diameter of a closed ball of radius r is at most 2 r.

theorem Metric.diam_ball {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h : 0 ≤ r) : Metric.diam (Metric.ball x r) ≤ 2 * r

The diameter of a ball of radius r is at most 2 r.

theorem IsComplete.nonempty_iInter_of_nonempty_biInter {α : Type u} [PseudoMetricSpace α] {s : ℕ → Set α} (h0 : IsComplete (s 0)) (hs : ∀ (n : ℕ), IsClosed (s n)) (h's : ∀ (n : ℕ), Bornology.IsBounded (s n)) (h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)) (h' : Filter.Tendsto (fun n => Metric.diam (s n)) Filter.atTop (nhds 0)) : Set.Nonempty (⋂ (n : ℕ), s n)

If a family of complete sets with diameter tending to 0 is such that each finite intersection is nonempty, then the total intersection is also nonempty.

theorem Metric.nonempty_iInter_of_nonempty_biInter {α : Type u} [PseudoMetricSpace α] [CompleteSpace α] {s : ℕ → Set α} (hs : ∀ (n : ℕ), IsClosed (s n)) (h's : ∀ (n : ℕ), Bornology.IsBounded (s n)) (h : ∀ (N : ℕ), Set.Nonempty (⋂ (n : ℕ) (_ : n ≤ N), s n)) (h' : Filter.Tendsto (fun n => Metric.diam (s n)) Filter.atTop (nhds 0)) : Set.Nonempty (⋂ (n : ℕ), s n)

In a complete space, if a family of closed sets with diameter tending to 0 is such that each finite intersection is nonempty, then the total intersection is also nonempty.

theorem Metric.exists_isLocalMin_mem_ball {α : Type u} {β : Type v} [PseudoMetricSpace α] [ProperSpace α] [TopologicalSpace β] [ConditionallyCompleteLinearOrder β] [OrderTopology β] {f : α → β} {a : α} {z : α} {r : ℝ} (hf : ContinuousOn f (Metric.closedBall a r)) (hz : z ∈ Metric.closedBall a r) (hf1 : ∀ (z' : α), z' ∈ Metric.sphere a r → f z < f z') : ∃ z, z ∈ Metric.ball a r ∧ IsLocalMin f z

def Mathlib.Meta.Positivity.evalDiam : Mathlib.Meta.Positivity.PositivityExt

Extension for the positivity tactic: the diameter of a set is always nonnegative.

Equations

• One or more equations did not get rendered due to their size.

theorem comap_dist_right_atTop_le_cocompact {α : Type u} [PseudoMetricSpace α] (x : α) : Filter.comap (fun y => dist y x) Filter.atTop ≤ Filter.cocompact α

theorem comap_dist_left_atTop_le_cocompact {α : Type u} [PseudoMetricSpace α] (x : α) : Filter.comap (dist x) Filter.atTop ≤ Filter.cocompact α

theorem comap_dist_right_atTop_eq_cocompact {α : Type u} [PseudoMetricSpace α] [ProperSpace α] (x : α) : Filter.comap (fun y => dist y x) Filter.atTop = Filter.cocompact α

theorem comap_dist_left_atTop_eq_cocompact {α : Type u} [PseudoMetricSpace α] [ProperSpace α] (x : α) : Filter.comap (dist x) Filter.atTop = Filter.cocompact α

theorem tendsto_cocompact_of_tendsto_dist_comp_atTop {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {l : Filter β} (x : α) (h : Filter.Tendsto (fun y => dist (f y) x) l Filter.atTop) : Filter.Tendsto f l (Filter.cocompact α)

class MetricSpace (α : Type u) extends PseudoMetricSpace : Type u

• dist : α → α → ℝ
• dist_self : ∀ (x : α), dist x x = 0
• dist_comm : ∀ (x y : α), dist x y = dist y x
• dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z
• edist : α → α → ENNReal
• edist_dist : ∀ (x y : α), PseudoMetricSpace.edist x y = ENNReal.ofReal (dist x y)
• toUniformSpace : UniformSpace α
• uniformity_dist : uniformity α = ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
• toBornology : Bornology α
• cobounded_sets : (Bornology.cobounded α).sets = {s_1 | ∃ C, ∀ (x : α), x ∈ s_1ᶜ → ∀ (y : α), y ∈ s_1ᶜ → dist x y ≤ C}
• eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y

We now define MetricSpace, extending PseudoMetricSpace.

theorem MetricSpace.ext {α : Type u_3} {m : MetricSpace α} {m' : MetricSpace α} (h : PseudoMetricSpace.toDist = PseudoMetricSpace.toDist) : m = m'

Two metric space structures with the same distance coincide.

def MetricSpace.ofDistTopology {α : Type u} [TopologicalSpace α] (dist : α → α → ℝ) (dist_self : ∀ (x : α), dist x x = 0) (dist_comm : ∀ (x y : α), dist x y = dist y x) (dist_triangle : ∀ (x y z : α), dist x z ≤ dist x y + dist y z) (H : ∀ (s : Set α), IsOpen s ↔ ∀ (x : α), x ∈ s → ∃ ε, ε > 0 ∧ ∀ (y : α), dist x y < ε → y ∈ s) (eq_of_dist_eq_zero : ∀ (x y : α), dist x y = 0 → x = y) : MetricSpace α

Construct a metric space structure whose underlying topological space structure (definitionally) agrees which a pre-existing topology which is compatible with a given distance function.

Equations

• One or more equations did not get rendered due to their size.

theorem eq_of_dist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} : dist x y = 0 → x = y

@[simp]

theorem dist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} : dist x y = 0 ↔ x = y

@[simp]

theorem zero_eq_dist {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} : 0 = dist x y ↔ x = y

theorem dist_ne_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} : dist x y ≠ 0 ↔ x ≠ y

@[simp]

theorem dist_le_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} : dist x y ≤ 0 ↔ x = y

@[simp]

theorem dist_pos {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} : 0 < dist x y ↔ x ≠ y

theorem eq_of_forall_dist_le {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} (h : ∀ (ε : ℝ), ε > 0 → dist x y ≤ ε) : x = y

theorem eq_of_nndist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} : nndist x y = 0 → x = y

Deduce the equality of points with the vanishing of the nonnegative distance

@[simp]

theorem nndist_eq_zero {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} : nndist x y = 0 ↔ x = y

Characterize the equality of points with the vanishing of the nonnegative distance

@[simp]

theorem zero_eq_nndist {γ : Type w} [MetricSpace γ] {x : γ} {y : γ} : 0 = nndist x y ↔ x = y

@[simp]

theorem Metric.closedBall_zero {γ : Type w} [MetricSpace γ] {x : γ} : Metric.closedBall x 0 = {x}

@[simp]

theorem Metric.sphere_zero {γ : Type w} [MetricSpace γ] {x : γ} : Metric.sphere x 0 = {x}

theorem Metric.subsingleton_closedBall {γ : Type w} [MetricSpace γ] (x : γ) {r : ℝ} (hr : r ≤ 0) : Set.Subsingleton (Metric.closedBall x r)

theorem Metric.subsingleton_sphere {γ : Type w} [MetricSpace γ] (x : γ) {r : ℝ} (hr : r ≤ 0) : Set.Subsingleton (Metric.sphere x r)

instance MetricSpace.to_separated {γ : Type w} [MetricSpace γ] : SeparatedSpace γ

Equations

• @MetricSpace.to_separated = @MetricSpace.to_separated.proof_1

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]

def MetricSpace.ofT0PseudoMetricSpace (α : Type u_3) [PseudoMetricSpace α] [T0Space α] : MetricSpace α

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

Equations

• MetricSpace.ofT0PseudoMetricSpace α = MetricSpace.mk (_ : ∀ {x y : α}, dist x y = 0 → x = y)

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 : Set.Pairwise s fun x y => ε ≤ dist x y) : IsClosed s

theorem Metric.closedEmbedding_of_pairwise_le_dist {γ : Type w} [MetricSpace γ] {α : Type u_3} [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_3} {ε : ℝ} (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 β.

theorem Metric.finite_isBounded_inter_isClosed {α : Type u} [PseudoMetricSpace α] [ProperSpace α] {K : Set α} {s : Set α} [DiscreteTopology ↑s] (hK : Bornology.IsBounded K) (hs : IsClosed s) : Set.Finite (K ∩ s)

def MetricSpace.replaceUniformity {γ : Type u_3} [U : UniformSpace γ] (m : MetricSpace γ) (H : uniformity γ = uniformity γ) : MetricSpace γ

Build a new metric space from an old one where the bundled uniform structure is provably (but typically non-definitionaly) equal to some given uniform structure. See Note [forgetful inheritance].

Equations

• MetricSpace.replaceUniformity m H = MetricSpace.mk (_ : ∀ {x y : γ}, dist x y = 0 → x = y)

theorem MetricSpace.replaceUniformity_eq {γ : Type u_3} [U : UniformSpace γ] (m : MetricSpace γ) (H : uniformity γ = uniformity γ) : MetricSpace.replaceUniformity m H = m

@[reducible]

def MetricSpace.replaceTopology {γ : Type u_3} [U : TopologicalSpace γ] (m : MetricSpace γ) (H : U = UniformSpace.toTopologicalSpace) : MetricSpace γ

Build a new metric space from an old one where the bundled topological structure is provably (but typically non-definitionaly) equal to some given topological structure. See Note [forgetful inheritance].

Equations

• MetricSpace.replaceTopology m H = MetricSpace.replaceUniformity m (_ : uniformity γ = uniformity γ)

theorem MetricSpace.replaceTopology_eq {γ : Type u_3} [U : TopologicalSpace γ] (m : MetricSpace γ) (H : U = UniformSpace.toTopologicalSpace) : MetricSpace.replaceTopology m H = m

@[reducible]

def EMetricSpace.toMetricSpaceOfDist {α : Type u} [EMetricSpace α] (dist : α → α → ℝ) (edist_ne_top : ∀ (x y : α), edist x y ≠ ⊤) (h : ∀ (x y : α), dist x y = ENNReal.toReal (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. 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

• One or more equations did not get rendered due to their size.

def MetricSpace.replaceBornology {α : Type u_3} [B : Bornology α] (m : MetricSpace α) (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) : MetricSpace α

Build a new metric space from an old one where the bundled bornology structure is provably (but typically non-definitionaly) equal to some given bornology structure. See Note [forgetful inheritance].

Equations

• MetricSpace.replaceBornology m H = let src := PseudoMetricSpace.replaceBornology MetricSpace.toPseudoMetricSpace H; MetricSpace.mk (_ : ∀ {x y : α}, dist x y = 0 → x = y)

theorem MetricSpace.replaceBornology_eq {α : Type u_3} [m : MetricSpace α] [B : Bornology α] (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) : MetricSpace.replaceBornology m H = m

@[reducible]

def MetricSpace.induced {γ : Type u_3} {β : Type u_4} (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 = let src := PseudoMetricSpace.induced f MetricSpace.toPseudoMetricSpace; MetricSpace.mk (_ : ∀ {x y : γ}, dist x y = 0 → x = y)

@[reducible]

def UniformEmbedding.comapMetricSpace {α : Type u_3} {β : Type u_4} [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

• One or more equations did not get rendered due to their size.

@[reducible]

def Embedding.comapMetricSpace {α : Type u_3} {β : Type u_4} [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.replaceTopology (MetricSpace.induced f (_ : Function.Injective f) m) (_ : inst = TopologicalSpace.induced f UniformSpace.toTopologicalSpace)

instance Subtype.metricSpace {α : Type u_3} {p : α → Prop} [MetricSpace α] : MetricSpace (Subtype p)

Equations

• Subtype.metricSpace = MetricSpace.induced Subtype.val (_ : Function.Injective fun a => ↑a) inst

instance instMetricSpaceAddOpposite {α : Type u_3} [MetricSpace α] : MetricSpace αᵃᵒᵖ

Equations

• instMetricSpaceAddOpposite = MetricSpace.induced AddOpposite.unop (_ : Function.Injective AddOpposite.unop) inst

instance instMetricSpaceMulOpposite {α : Type u_3} [MetricSpace α] : MetricSpace αᵐᵒᵖ

Equations

• instMetricSpaceMulOpposite = MetricSpace.induced MulOpposite.unop (_ : Function.Injective MulOpposite.unop) inst

instance instMetricSpaceEmpty : MetricSpace Empty

Equations

• instMetricSpaceEmpty = MetricSpace.mk (_ : ∀ {x y : Empty}, dist x y = 0 → x = y)

instance instMetricSpacePUnit : MetricSpace PUnit.{u + 1}

Equations

• instMetricSpacePUnit = MetricSpace.mk (_ : ∀ {x y : PUnit.{u + 1} }, dist x y = 0 → x = y)

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_3, v} β)

Equations

• instMetricSpaceULift = MetricSpace.induced ULift.down (_ : Function.Injective ULift.down) inst

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

Equations

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

instance metricSpacePi {β : Type v} {π : β → Type u_3} [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 → ∃ β x F, ∀ (x y : α), F x = F y → dist x y ≤ ε) : TopologicalSpace.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 instDistSeparationQuotientToUniformSpace {α : Type u} [PseudoMetricSpace α] : Dist (UniformSpace.SeparationQuotient α)

Equations

• instDistSeparationQuotientToUniformSpace = { dist := fun p q => Quotient.liftOn₂' p q dist (_ : ∀ (x y x' y' : α), Setoid.r x x' → Setoid.r y y' → dist x y = dist x' y') }

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

instance instMetricSpaceSeparationQuotientToUniformSpace {α : Type u} [PseudoMetricSpace α] : MetricSpace (UniformSpace.SeparationQuotient α)

Equations

• One or more equations did not get rendered due to their size.

Additive, Multiplicative

The distance on those type synonyms is inherited without change.

instance instDistAdditive {X : Type u_1} [Dist X] : Dist (Additive X)

Equations

• instDistAdditive = inst

instance instDistMultiplicative {X : Type u_1} [Dist X] : Dist (Multiplicative X)

Equations

• instDistMultiplicative = inst

@[simp]

theorem dist_ofMul {X : Type u_1} [Dist X] (a : X) (b : X) : dist (↑Additive.ofMul a) (↑Additive.ofMul b) = dist a b

@[simp]

theorem dist_ofAdd {X : Type u_1} [Dist X] (a : X) (b : X) : dist (↑Multiplicative.ofAdd a) (↑Multiplicative.ofAdd b) = dist a b

@[simp]

theorem dist_toMul {X : Type u_1} [Dist X] (a : Additive X) (b : Additive X) : dist (↑Additive.toMul a) (↑Additive.toMul b) = dist a b

@[simp]

theorem dist_toAdd {X : Type u_1} [Dist X] (a : Multiplicative X) (b : Multiplicative X) : dist (↑Multiplicative.toAdd a) (↑Multiplicative.toAdd b) = dist a b

instance instPseudoMetricSpaceAdditive {X : Type u_1} [PseudoMetricSpace X] : PseudoMetricSpace (Additive X)

Equations

• instPseudoMetricSpaceAdditive = inst

instance instPseudoMetricSpaceMultiplicative {X : Type u_1} [PseudoMetricSpace X] : PseudoMetricSpace (Multiplicative X)

Equations

• instPseudoMetricSpaceMultiplicative = inst

@[simp]

theorem nndist_ofMul {X : Type u_1} [PseudoMetricSpace X] (a : X) (b : X) : nndist (↑Additive.ofMul a) (↑Additive.ofMul b) = nndist a b

@[simp]

theorem nndist_ofAdd {X : Type u_1} [PseudoMetricSpace X] (a : X) (b : X) : nndist (↑Multiplicative.ofAdd a) (↑Multiplicative.ofAdd b) = nndist a b

@[simp]

theorem nndist_toMul {X : Type u_1} [PseudoMetricSpace X] (a : Additive X) (b : Additive X) : nndist (↑Additive.toMul a) (↑Additive.toMul b) = nndist a b

@[simp]

theorem nndist_toAdd {X : Type u_1} [PseudoMetricSpace X] (a : Multiplicative X) (b : Multiplicative X) : nndist (↑Multiplicative.toAdd a) (↑Multiplicative.toAdd b) = nndist a b

instance instMetricSpaceAdditive {X : Type u_1} [MetricSpace X] : MetricSpace (Additive X)

Equations

• instMetricSpaceAdditive = inst

instance instMetricSpaceMultiplicative {X : Type u_1} [MetricSpace X] : MetricSpace (Multiplicative X)

Equations

• instMetricSpaceMultiplicative = inst

instance instProperSpaceAdditiveInstPseudoMetricSpaceAdditive {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] : ProperSpace (Additive X)

Equations

• (_ : ProperSpace (Additive X)) = inst

instance instProperSpaceMultiplicativeInstPseudoMetricSpaceMultiplicative {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] : ProperSpace (Multiplicative X)

Equations

• (_ : ProperSpace (Multiplicative X)) = inst

Order dual

The distance on this type synonym is inherited without change.

instance instDistOrderDual {X : Type u_1} [Dist X] : Dist Xᵒᵈ

Equations

• instDistOrderDual = inst

@[simp]

theorem dist_toDual {X : Type u_1} [Dist X] (a : X) (b : X) : dist (↑OrderDual.toDual a) (↑OrderDual.toDual b) = dist a b

@[simp]

theorem dist_ofDual {X : Type u_1} [Dist X] (a : Xᵒᵈ) (b : Xᵒᵈ) : dist (↑OrderDual.ofDual a) (↑OrderDual.ofDual b) = dist a b

instance instPseudoMetricSpaceOrderDual {X : Type u_1} [PseudoMetricSpace X] : PseudoMetricSpace Xᵒᵈ

Equations

• instPseudoMetricSpaceOrderDual = inst

@[simp]

theorem nndist_toDual {X : Type u_1} [PseudoMetricSpace X] (a : X) (b : X) : nndist (↑OrderDual.toDual a) (↑OrderDual.toDual b) = nndist a b

@[simp]

theorem nndist_ofDual {X : Type u_1} [PseudoMetricSpace X] (a : Xᵒᵈ) (b : Xᵒᵈ) : nndist (↑OrderDual.ofDual a) (↑OrderDual.ofDual b) = nndist a b

instance instMetricSpaceOrderDual {X : Type u_1} [MetricSpace X] : MetricSpace Xᵒᵈ

Equations

• instMetricSpaceOrderDual = inst

instance instProperSpaceOrderDualInstPseudoMetricSpaceOrderDual {X : Type u_1} [PseudoMetricSpace X] [ProperSpace X] : ProperSpace Xᵒᵈ

Equations

• (_ : ProperSpace Xᵒᵈ) = inst