Extended metric spaces

This file is devoted to the definition and study of EMetricSpaces, i.e., metric spaces in which the distance is allowed to take the value ∞. This extended distance is called edist, and takes values in ℝ≥0∞.

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

The class EMetricSpace therefore extends UniformSpace (and TopologicalSpace).

Since a lot of elementary properties don't require eq_of_edist_eq_zero we start setting up the theory of PseudoEMetricSpace, where we don't require edist x y = 0 → x = y and we specialize to EMetricSpace at the end.

theorem uniformity_dist_of_mem_uniformity {α : Type u} {β : Type v} [LinearOrder β] {U : Filter (α × α)} (z : β) (D : α → α → β) (H : ∀ (s : Set (α × α)), s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s) : U = ⨅ (ε : β), ⨅ (_ : ε > z), Filter.principal {p : α × α | D p.1 p.2 < ε}

Characterizing uniformities associated to a (generalized) distance function D in terms of the elements of the uniformity.

class EDist (α : Type u_2) : Type u_2

EDist α means that α is equipped with an extended distance.

• edist : α → α → ENNReal

def uniformSpaceOfEDist {α : Type u} (edist : α → α → ENNReal) (edist_self : ∀ (x : α), edist x x = 0) (edist_comm : ∀ (x y : α), edist x y = edist y x) (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) : UniformSpace α

Creating a uniform space from an extended distance.

Equations

• uniformSpaceOfEDist edist edist_self edist_comm edist_triangle = UniformSpace.ofFun edist edist_self edist_comm edist_triangle uniformSpaceOfEDist.proof_1

class PseudoEMetricSpace (α : Type u) extends EDist : Type u

Extended (pseudo) metric spaces, with an extended distance edist possibly taking the value ∞

Each pseudo_emetric 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 PseudoEMetricSpace structure, the uniformity fields are not necessary, they will be filled in by default. There is a default value for the uniformity, that can be substituted in cases of interest, for instance when instantiating a PseudoEMetricSpace structure on a product.

Continuity of edist is proved in Topology.Instances.ENNReal

• edist : α → α → ENNReal
• edist_self : ∀ (x : α), edist x x = 0
• edist_comm : ∀ (x y : α), edist x y = edist y x
• edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
• toUniformSpace : UniformSpace α
• uniformity_edist : uniformity α = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : α × α | edist p.1 p.2 < ε}

theorem edist_triangle_left {α : Type u} [PseudoEMetricSpace α] (x : α) (y : α) (z : α) : edist x y ≤ edist z x + edist z y

Triangle inequality for the extended distance

theorem edist_triangle_right {α : Type u} [PseudoEMetricSpace α] (x : α) (y : α) (z : α) : edist x y ≤ edist x z + edist y z

theorem edist_congr_right {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {z : α} (h : edist x y = 0) : edist x z = edist y z

theorem edist_congr_left {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {z : α} (h : edist x y = 0) : edist z x = edist z y

theorem edist_congr {α : Type u} [PseudoEMetricSpace α] {w : α} {x : α} {y : α} {z : α} (hl : edist w x = 0) (hr : edist y z = 0) : edist w y = edist x z

theorem edist_triangle4 {α : Type u} [PseudoEMetricSpace α] (x : α) (y : α) (z : α) (t : α) : edist x t ≤ edist x y + edist y z + edist z t

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

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

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

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

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

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

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

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

theorem uniformity_pseudoedist {α : Type u} [PseudoEMetricSpace α] : uniformity α = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : α × α | edist p.1 p.2 < ε}

Reformulation of the uniform structure in terms of the extended distance

theorem uniformSpace_edist {α : Type u} [PseudoEMetricSpace α] : PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist (_ : ∀ (x : α), edist x x = 0) (_ : ∀ (x y : α), edist x y = edist y x) (_ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z)

theorem uniformity_basis_edist {α : Type u} [PseudoEMetricSpace α] : Filter.HasBasis (uniformity α) (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 < ε}

theorem mem_uniformity_edist {α : Type u} [PseudoEMetricSpace α] {s : Set (α × α)} : s ∈ uniformity α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s

Characterization of the elements of the uniformity in terms of the extended distance

theorem EMetric.mk_uniformity_basis {α : Type u} [PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal} (hf₀ : ∀ (x : β), p x → 0 < f x) (hf : ∀ (ε : ENNReal), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε) : Filter.HasBasis (uniformity α) p fun (x : β) => {p : α × α | edist p.1 p.2 < f x}

Given f : β → ℝ≥0∞, 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_edist, uniformity_basis_edist', uniformity_basis_edist_nnreal, and uniformity_basis_edist_inv_nat.

theorem EMetric.mk_uniformity_basis_le {α : Type u} [PseudoEMetricSpace α] {β : Type u_2} {p : β → Prop} {f : β → ENNReal} (hf₀ : ∀ (x : β), p x → 0 < f x) (hf : ∀ (ε : ENNReal), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε) : Filter.HasBasis (uniformity α) p fun (x : β) => {p : α × α | edist p.1 p.2 ≤ f x}

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

For specific bases see uniformity_basis_edist_le and uniformity_basis_edist_le'.

theorem uniformity_basis_edist_le {α : Type u} [PseudoEMetricSpace α] : Filter.HasBasis (uniformity α) (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 ≤ ε}

theorem uniformity_basis_edist' {α : Type u} [PseudoEMetricSpace α] (ε' : ENNReal) (hε' : 0 < ε') : Filter.HasBasis (uniformity α) (fun (ε : ENNReal) => ε ∈ Set.Ioo 0 ε') fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 < ε}

theorem uniformity_basis_edist_le' {α : Type u} [PseudoEMetricSpace α] (ε' : ENNReal) (hε' : 0 < ε') : Filter.HasBasis (uniformity α) (fun (ε : ENNReal) => ε ∈ Set.Ioo 0 ε') fun (ε : ENNReal) => {p : α × α | edist p.1 p.2 ≤ ε}

theorem uniformity_basis_edist_nnreal {α : Type u} [PseudoEMetricSpace α] : Filter.HasBasis (uniformity α) (fun (ε : NNReal) => 0 < ε) fun (ε : NNReal) => {p : α × α | edist p.1 p.2 < ↑ε}

theorem uniformity_basis_edist_nnreal_le {α : Type u} [PseudoEMetricSpace α] : Filter.HasBasis (uniformity α) (fun (ε : NNReal) => 0 < ε) fun (ε : NNReal) => {p : α × α | edist p.1 p.2 ≤ ↑ε}

theorem uniformity_basis_edist_inv_nat {α : Type u} [PseudoEMetricSpace α] : Filter.HasBasis (uniformity α) (fun (x : ℕ) => True) fun (n : ℕ) => {p : α × α | edist p.1 p.2 < (↑n)⁻¹}

theorem uniformity_basis_edist_inv_two_pow {α : Type u} [PseudoEMetricSpace α] : Filter.HasBasis (uniformity α) (fun (x : ℕ) => True) fun (n : ℕ) => {p : α × α | edist p.1 p.2 < 2⁻¹ ^ n}

theorem edist_mem_uniformity {α : Type u} [PseudoEMetricSpace α] {ε : ENNReal} (ε0 : 0 < ε) : {p : α × α | edist p.1 p.2 < ε} ∈ uniformity α

Fixed size neighborhoods of the diagonal belong to the uniform structure

instance EMetric.instIsCountablyGeneratedUniformity {α : Type u} [PseudoEMetricSpace α] : Filter.IsCountablyGenerated (uniformity α)

Equations

• (_ : Filter.IsCountablyGenerated (uniformity α)) = (_ : Filter.IsCountablyGenerated (uniformity α))

theorem EMetric.uniformContinuousOn_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a : α}, a ∈ s → ∀ {b : α}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε

ε-δ characterization of uniform continuity on a set for pseudoemetric spaces

theorem EMetric.uniformContinuous_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} : UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε

ε-δ characterization of uniform continuity on pseudoemetric spaces

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

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

ε-δ characterization of uniform embeddings on pseudoemetric spaces

theorem EMetric.controlled_of_uniformEmbedding {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : UniformEmbedding f) : (∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ

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

In fact, this lemma holds for a UniformInducing map. TODO: generalize?

theorem EMetric.cauchy_iff {α : Type u} [PseudoEMetricSpace α] {f : Filter α} : Cauchy f ↔ f ≠ ⊥ ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, edist x y < ε

ε-δ characterization of Cauchy sequences on pseudoemetric spaces

theorem EMetric.complete_of_convergent_controlled_sequences {α : Type u} [PseudoEMetricSpace α] (B : ℕ → ENNReal) (hB : ∀ (n : ℕ), 0 < B n) (H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (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 edist (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 EMetric.complete_of_cauchySeq_tendsto {α : Type u} [PseudoEMetricSpace α] : (∀ (u : ℕ → α), CauchySeq u → ∃ (a : α), Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace α

A sequentially complete pseudoemetric space is complete.

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

Expressing locally uniform convergence on a set using edist.

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

Expressing uniform convergence on a set using edist.

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

Expressing locally uniform convergence using edist.

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

Expressing uniform convergence using edist.

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

Auxiliary function to replace the uniformity on a pseudoemetric space with a uniformity which is equal to the original one, but maybe not defeq. This is useful if one wants to construct a pseudoemetric space with a specified uniformity. See Note [forgetful inheritance] explaining why having definitionally the right uniformity is often important.

Equations

• PseudoEMetricSpace.replaceUniformity m H = PseudoEMetricSpace.mk (_ : ∀ (x : α), edist x x = 0) (_ : ∀ (x y : α), edist x y = edist y x) (_ : ∀ (x y z : α), edist x z ≤ edist x y + edist y z) U

def PseudoEMetricSpace.induced {α : Type u_2} {β : Type u_3} (f : α → β) (m : PseudoEMetricSpace β) : PseudoEMetricSpace α

The extended pseudometric induced by a function taking values in a pseudoemetric space.

Equations

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

instance instPseudoEMetricSpaceSubtype {α : Type u_2} {p : α → Prop} [PseudoEMetricSpace α] : PseudoEMetricSpace (Subtype p)

Pseudoemetric space instance on subsets of pseudoemetric spaces

Equations

• instPseudoEMetricSpaceSubtype = PseudoEMetricSpace.induced Subtype.val inst

theorem Subtype.edist_eq {α : Type u} [PseudoEMetricSpace α] {p : α → Prop} (x : Subtype p) (y : Subtype p) : edist x y = edist ↑x ↑y

The extended pseudodistance on a subset of a pseudoemetric space is the restriction of the original pseudodistance, by definition

instance AddOpposite.instPseudoEMetricSpaceAddOpposite {α : Type u_2} [PseudoEMetricSpace α] : PseudoEMetricSpace αᵃᵒᵖ

Pseudoemetric space instance on the additive opposite of a pseudoemetric space.

Equations

• AddOpposite.instPseudoEMetricSpaceAddOpposite = PseudoEMetricSpace.induced AddOpposite.unop inst

instance MulOpposite.instPseudoEMetricSpaceMulOpposite {α : Type u_2} [PseudoEMetricSpace α] : PseudoEMetricSpace αᵐᵒᵖ

Pseudoemetric space instance on the multiplicative opposite of a pseudoemetric space.

Equations

• MulOpposite.instPseudoEMetricSpaceMulOpposite = PseudoEMetricSpace.induced MulOpposite.unop inst

theorem AddOpposite.edist_unop {α : Type u} [PseudoEMetricSpace α] (x : αᵃᵒᵖ) (y : αᵃᵒᵖ) : edist (AddOpposite.unop x) (AddOpposite.unop y) = edist x y

theorem MulOpposite.edist_unop {α : Type u} [PseudoEMetricSpace α] (x : αᵐᵒᵖ) (y : αᵐᵒᵖ) : edist (MulOpposite.unop x) (MulOpposite.unop y) = edist x y

theorem AddOpposite.edist_op {α : Type u} [PseudoEMetricSpace α] (x : α) (y : α) : edist (AddOpposite.op x) (AddOpposite.op y) = edist x y

theorem MulOpposite.edist_op {α : Type u} [PseudoEMetricSpace α] (x : α) (y : α) : edist (MulOpposite.op x) (MulOpposite.op y) = edist x y

instance instPseudoEMetricSpaceULift {α : Type u} [PseudoEMetricSpace α] : PseudoEMetricSpace (ULift.{u_2, u} α)

Equations

• instPseudoEMetricSpaceULift = PseudoEMetricSpace.induced ULift.down inst

theorem ULift.edist_eq {α : Type u} [PseudoEMetricSpace α] (x : ULift.{u_2, u} α) (y : ULift.{u_2, u} α) : edist x y = edist x.down y.down

@[simp]

theorem ULift.edist_up_up {α : Type u} [PseudoEMetricSpace α] (x : α) (y : α) : edist { down := x } { down := y } = edist x y

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

The product of two pseudoemetric spaces, with the max distance, is an extended pseudometric spaces. We make sure that the uniform structure thus constructed is the one corresponding to the product of uniform spaces, to avoid diamond problems.

Equations

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

theorem Prod.edist_eq {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x : α × β) (y : α × β) : edist x y = max (edist x.1 y.1) (edist x.2 y.2)

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

Equations

• instEDistForAll = { edist := fun (f g : (b : β) → π b) => Finset.sup Finset.univ fun (b : β) => edist (f b) (g b) }

theorem edist_pi_def {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EDist (π b)] (f : (b : β) → π b) (g : (b : β) → π b) : edist f g = Finset.sup Finset.univ fun (b : β) => edist (f b) (g b)

theorem edist_le_pi_edist {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EDist (π b)] (f : (b : β) → π b) (g : (b : β) → π b) (b : β) : edist (f b) (g b) ≤ edist f g

theorem edist_pi_le_iff {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → EDist (π b)] {f : (b : β) → π b} {g : (b : β) → π b} {d : ENNReal} : edist f g ≤ d ↔ ∀ (b : β), edist (f b) (g b) ≤ d

theorem edist_pi_const_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Fintype β] (a : α) (b : α) : (edist (fun (x : β) => a) fun (x : β) => b) ≤ edist a b

@[simp]

theorem edist_pi_const {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Fintype β] [Nonempty β] (a : α) (b : α) : (edist (fun (x : β) => a) fun (x : β) => b) = edist a b

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

The product of a finite number of pseudoemetric spaces, with the max distance, is still a pseudoemetric space. This construction would also work for infinite products, but it would not give rise to the product topology. Hence, we only formalize it in the good situation of finitely many spaces.

Equations

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

def EMetric.ball {α : Type u} [PseudoEMetricSpace α] (x : α) (ε : ENNReal) : Set α

EMetric.ball x ε is the set of all points y with edist y x < ε

Equations

• EMetric.ball x ε = {y : α | edist y x < ε}

@[simp]

theorem EMetric.mem_ball {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {ε : ENNReal} : y ∈ EMetric.ball x ε ↔ edist y x < ε

theorem EMetric.mem_ball' {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {ε : ENNReal} : y ∈ EMetric.ball x ε ↔ edist x y < ε

def EMetric.closedBall {α : Type u} [PseudoEMetricSpace α] (x : α) (ε : ENNReal) : Set α

EMetric.closedBall x ε is the set of all points y with edist y x ≤ ε

Equations

• EMetric.closedBall x ε = {y : α | edist y x ≤ ε}

@[simp]

theorem EMetric.mem_closedBall {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {ε : ENNReal} : y ∈ EMetric.closedBall x ε ↔ edist y x ≤ ε

theorem EMetric.mem_closedBall' {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {ε : ENNReal} : y ∈ EMetric.closedBall x ε ↔ edist x y ≤ ε

@[simp]

theorem EMetric.closedBall_top {α : Type u} [PseudoEMetricSpace α] (x : α) : EMetric.closedBall x ⊤ = Set.univ

theorem EMetric.ball_subset_closedBall {α : Type u} [PseudoEMetricSpace α] {x : α} {ε : ENNReal} : EMetric.ball x ε ⊆ EMetric.closedBall x ε

theorem EMetric.pos_of_mem_ball {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {ε : ENNReal} (hy : y ∈ EMetric.ball x ε) : 0 < ε

theorem EMetric.mem_ball_self {α : Type u} [PseudoEMetricSpace α] {x : α} {ε : ENNReal} (h : 0 < ε) : x ∈ EMetric.ball x ε

theorem EMetric.mem_closedBall_self {α : Type u} [PseudoEMetricSpace α] {x : α} {ε : ENNReal} : x ∈ EMetric.closedBall x ε

theorem EMetric.mem_ball_comm {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {ε : ENNReal} : x ∈ EMetric.ball y ε ↔ y ∈ EMetric.ball x ε

theorem EMetric.mem_closedBall_comm {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {ε : ENNReal} : x ∈ EMetric.closedBall y ε ↔ y ∈ EMetric.closedBall x ε

theorem EMetric.ball_subset_ball {α : Type u} [PseudoEMetricSpace α] {x : α} {ε₁ : ENNReal} {ε₂ : ENNReal} (h : ε₁ ≤ ε₂) : EMetric.ball x ε₁ ⊆ EMetric.ball x ε₂

theorem EMetric.closedBall_subset_closedBall {α : Type u} [PseudoEMetricSpace α] {x : α} {ε₁ : ENNReal} {ε₂ : ENNReal} (h : ε₁ ≤ ε₂) : EMetric.closedBall x ε₁ ⊆ EMetric.closedBall x ε₂

theorem EMetric.ball_disjoint {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {ε₁ : ENNReal} {ε₂ : ENNReal} (h : ε₁ + ε₂ ≤ edist x y) : Disjoint (EMetric.ball x ε₁) (EMetric.ball y ε₂)

theorem EMetric.ball_subset {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {ε₁ : ENNReal} {ε₂ : ENNReal} (h : edist x y + ε₁ ≤ ε₂) (h' : edist x y ≠ ⊤) : EMetric.ball x ε₁ ⊆ EMetric.ball y ε₂

theorem EMetric.exists_ball_subset_ball {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {ε : ENNReal} (h : y ∈ EMetric.ball x ε) : ∃ ε' > 0, EMetric.ball y ε' ⊆ EMetric.ball x ε

theorem EMetric.ball_eq_empty_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {ε : ENNReal} : EMetric.ball x ε = ∅ ↔ ε = 0

theorem EMetric.ordConnected_setOf_closedBall_subset {α : Type u} [PseudoEMetricSpace α] (x : α) (s : Set α) : Set.OrdConnected {r : ENNReal | EMetric.closedBall x r ⊆ s}

theorem EMetric.ordConnected_setOf_ball_subset {α : Type u} [PseudoEMetricSpace α] (x : α) (s : Set α) : Set.OrdConnected {r : ENNReal | EMetric.ball x r ⊆ s}

def EMetric.edistLtTopSetoid {α : Type u} [PseudoEMetricSpace α] : Setoid α

Relation “two points are at a finite edistance” is an equivalence relation.

Equations

• EMetric.edistLtTopSetoid = { r := fun (x y : α) => edist x y < ⊤, iseqv := (_ : Equivalence fun (x y : α) => edist x y < ⊤) }

@[simp]

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

theorem EMetric.nhds_basis_eball {α : Type u} [PseudoEMetricSpace α] {x : α} : Filter.HasBasis (nhds x) (fun (ε : ENNReal) => 0 < ε) (EMetric.ball x)

theorem EMetric.nhdsWithin_basis_eball {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} : Filter.HasBasis (nhdsWithin x s) (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => EMetric.ball x ε ∩ s

theorem EMetric.nhds_basis_closed_eball {α : Type u} [PseudoEMetricSpace α] {x : α} : Filter.HasBasis (nhds x) (fun (ε : ENNReal) => 0 < ε) (EMetric.closedBall x)

theorem EMetric.nhdsWithin_basis_closed_eball {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} : Filter.HasBasis (nhdsWithin x s) (fun (ε : ENNReal) => 0 < ε) fun (ε : ENNReal) => EMetric.closedBall x ε ∩ s

theorem EMetric.nhds_eq {α : Type u} [PseudoEMetricSpace α] {x : α} : nhds x = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal (EMetric.ball x ε)

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

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

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

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

theorem EMetric.tendsto_nhds_nhds {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : α → β} {a : α} {b : β} : Filter.Tendsto f (nhds a) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, edist x a < δ → edist (f x) b < ε

theorem EMetric.isOpen_iff {α : Type u} [PseudoEMetricSpace α] {s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, EMetric.ball x ε ⊆ s

theorem EMetric.isOpen_ball {α : Type u} [PseudoEMetricSpace α] {x : α} {ε : ENNReal} : IsOpen (EMetric.ball x ε)

theorem EMetric.isClosed_ball_top {α : Type u} [PseudoEMetricSpace α] {x : α} : IsClosed (EMetric.ball x ⊤)

theorem EMetric.ball_mem_nhds {α : Type u} [PseudoEMetricSpace α] (x : α) {ε : ENNReal} (ε0 : 0 < ε) : EMetric.ball x ε ∈ nhds x

theorem EMetric.closedBall_mem_nhds {α : Type u} [PseudoEMetricSpace α] (x : α) {ε : ENNReal} (ε0 : 0 < ε) : EMetric.closedBall x ε ∈ nhds x

theorem EMetric.ball_prod_same {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal) : EMetric.ball x r ×ˢ EMetric.ball y r = EMetric.ball (x, y) r

theorem EMetric.closedBall_prod_same {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (x : α) (y : β) (r : ENNReal) : EMetric.closedBall x r ×ˢ EMetric.closedBall y r = EMetric.closedBall (x, y) r

theorem EMetric.mem_closure_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} : x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε

ε-characterization of the closure in pseudoemetric spaces

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

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

theorem EMetric.inseparable_iff {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} : Inseparable x y ↔ edist x y = 0

theorem EMetric.cauchySeq_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ ∀ ε > 0, ∃ (N : β), ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → edist (u m) (u n) < ε

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

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

A variation around the emetric characterization of Cauchy sequences

theorem EMetric.cauchySeq_iff_NNReal {α : Type u} {β : Type v} [PseudoEMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} : CauchySeq u ↔ ∀ (ε : NNReal), 0 < ε → ∃ (N : β), ∀ (n : β), N ≤ n → edist (u n) (u N) < ↑ε

A variation of the emetric characterization of Cauchy sequences that deals with ℝ≥0 upper bounds.

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

theorem EMetric.totallyBounded_iff' {α : Type u} [PseudoEMetricSpace α] {s : Set α} : TotallyBounded s ↔ ∀ ε > 0, ∃ t ⊆ s, Set.Finite t ∧ s ⊆ ⋃ y ∈ t, EMetric.ball y ε

theorem EMetric.subset_countable_closure_of_almost_dense_set {α : Type u} [PseudoEMetricSpace α] (s : Set α) (hs : ∀ ε > 0, ∃ (t : Set α), Set.Countable t ∧ s ⊆ ⋃ x ∈ t, EMetric.closedBall x ε) : ∃ t ⊆ s, Set.Countable t ∧ s ⊆ closure t

For a set s in a pseudo emetric space, if for every ε > 0 there exists a countable set that is ε-dense in s, then there exists a countable subset t ⊆ s that is dense in s.

theorem TopologicalSpace.IsSeparable.exists_countable_dense_subset {α : Type u} [PseudoEMetricSpace α] {s : Set α} (hs : TopologicalSpace.IsSeparable s) : ∃ t ⊆ s, Set.Countable t ∧ s ⊆ closure t

If a set s is separable in a (pseudo extended) metric space, then it admits a countable dense subset. This is not obvious, as the countable set whose closure covers s given by the definition of separability does not need in general to be contained in s.

theorem TopologicalSpace.IsSeparable.separableSpace {α : Type u} [PseudoEMetricSpace α] {s : Set α} (hs : TopologicalSpace.IsSeparable s) : TopologicalSpace.SeparableSpace ↑s

If a set s is separable, then the corresponding subtype is separable in a (pseudo extended) metric space. This is not obvious, as the countable set whose closure covers s does not need in general to be contained in s.

theorem EMetric.subset_countable_closure_of_compact {α : Type u} [PseudoEMetricSpace α] {s : Set α} (hs : IsCompact s) : ∃ t ⊆ s, Set.Countable t ∧ s ⊆ closure t

A compact set in a pseudo emetric space is separable, i.e., it is a subset of the closure of a countable set.

instance EMetric.secondCountable_of_sigmaCompact (α : Type u) [PseudoEMetricSpace α] [SigmaCompactSpace α] : SecondCountableTopology α

A sigma compact pseudo emetric space has second countable topology.

Equations

• (_ : SecondCountableTopology α) = (_ : SecondCountableTopology α)

theorem EMetric.secondCountable_of_almost_dense_set {α : Type u} [PseudoEMetricSpace α] (hs : ∀ ε > 0, ∃ (t : Set α), Set.Countable t ∧ ⋃ x ∈ t, EMetric.closedBall x ε = Set.univ) : SecondCountableTopology α

noncomputable def EMetric.diam {α : Type u} [PseudoEMetricSpace α] (s : Set α) : ENNReal

The diameter of a set in a pseudoemetric space, named EMetric.diam

Equations

• EMetric.diam s = ⨆ x ∈ s, ⨆ y ∈ s, edist x y

theorem EMetric.diam_eq_sSup {α : Type u} [PseudoEMetricSpace α] (s : Set α) : EMetric.diam s = sSup (Set.image2 edist s s)

theorem EMetric.diam_le_iff {α : Type u} [PseudoEMetricSpace α] {s : Set α} {d : ENNReal} : EMetric.diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d

theorem EMetric.diam_image_le_iff {α : Type u} {β : Type v} [PseudoEMetricSpace α] {d : ENNReal} {f : β → α} {s : Set β} : EMetric.diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d

theorem EMetric.edist_le_of_diam_le {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {s : Set α} {d : ENNReal} (hx : x ∈ s) (hy : y ∈ s) (hd : EMetric.diam s ≤ d) : edist x y ≤ d

theorem EMetric.edist_le_diam_of_mem {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {s : Set α} (hx : x ∈ s) (hy : y ∈ s) : edist x y ≤ EMetric.diam s

If two points belong to some set, their edistance is bounded by the diameter of the set

theorem EMetric.diam_le {α : Type u} [PseudoEMetricSpace α] {s : Set α} {d : ENNReal} (h : ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d) : EMetric.diam s ≤ d

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

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

The diameter of a subsingleton vanishes.

@[simp]

theorem EMetric.diam_empty {α : Type u} [PseudoEMetricSpace α] : EMetric.diam ∅ = 0

The diameter of the empty set vanishes

@[simp]

theorem EMetric.diam_singleton {α : Type u} [PseudoEMetricSpace α] {x : α} : EMetric.diam {x} = 0

The diameter of a singleton vanishes

@[simp]

theorem EMetric.diam_zero {α : Type u} [PseudoEMetricSpace α] [Zero α] : EMetric.diam 0 = 0

@[simp]

theorem EMetric.diam_one {α : Type u} [PseudoEMetricSpace α] [One α] : EMetric.diam 1 = 0

theorem EMetric.diam_iUnion_mem_option {α : Type u} [PseudoEMetricSpace α] {ι : Type u_2} (o : Option ι) (s : ι → Set α) : EMetric.diam (⋃ i ∈ o, s i) = ⨆ i ∈ o, EMetric.diam (s i)

theorem EMetric.diam_insert {α : Type u} [PseudoEMetricSpace α] {x : α} {s : Set α} : EMetric.diam (insert x s) = max (⨆ y ∈ s, edist x y) (EMetric.diam s)

theorem EMetric.diam_pair {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} : EMetric.diam {x, y} = edist x y

theorem EMetric.diam_triple {α : Type u} [PseudoEMetricSpace α] {x : α} {y : α} {z : α} : EMetric.diam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)

theorem EMetric.diam_mono {α : Type u} [PseudoEMetricSpace α] {s : Set α} {t : Set α} (h : s ⊆ t) : EMetric.diam s ≤ EMetric.diam t

The diameter is monotonous with respect to inclusion

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

The diameter of a union is controlled by the diameter of the sets, and the edistance between two points in the sets.

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

theorem EMetric.diam_closedBall {α : Type u} [PseudoEMetricSpace α] {x : α} {r : ENNReal} : EMetric.diam (EMetric.closedBall x r) ≤ 2 * r

theorem EMetric.diam_ball {α : Type u} [PseudoEMetricSpace α] {x : α} {r : ENNReal} : EMetric.diam (EMetric.ball x r) ≤ 2 * r

theorem EMetric.diam_pi_le_of_le {β : Type v} {π : β → Type u_2} [Fintype β] [(b : β) → PseudoEMetricSpace (π b)] {s : (b : β) → Set (π b)} {c : ENNReal} (h : ∀ (b : β), EMetric.diam (s b) ≤ c) : EMetric.diam (Set.pi Set.univ s) ≤ c

class EMetricSpace (α : Type u) extends PseudoEMetricSpace : Type u

We now define EMetricSpace, extending PseudoEMetricSpace.

• edist : α → α → ENNReal
• edist_self : ∀ (x : α), edist x x = 0
• edist_comm : ∀ (x y : α), edist x y = edist y x
• edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z
• toUniformSpace : UniformSpace α
• uniformity_edist : uniformity α = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : α × α | edist p.1 p.2 < ε}
• eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y

@[simp]

theorem edist_eq_zero {γ : Type w} [EMetricSpace γ] {x : γ} {y : γ} : edist x y = 0 ↔ x = y

Characterize the equality of points by the vanishing of their extended distance

@[simp]

theorem zero_eq_edist {γ : Type w} [EMetricSpace γ] {x : γ} {y : γ} : 0 = edist x y ↔ x = y

theorem edist_le_zero {γ : Type w} [EMetricSpace γ] {x : γ} {y : γ} : edist x y ≤ 0 ↔ x = y

@[simp]

theorem edist_pos {γ : Type w} [EMetricSpace γ] {x : γ} {y : γ} : 0 < edist x y ↔ x ≠ y

theorem eq_of_forall_edist_le {γ : Type w} [EMetricSpace γ] {x : γ} {y : γ} (h : ∀ ε > 0, edist x y ≤ ε) : x = y

Two points coincide if their distance is < ε for all positive ε

instance to_separated {γ : Type w} [EMetricSpace γ] : SeparatedSpace γ

An emetric space is separated

Equations

• (_ : SeparatedSpace γ) = (_ : SeparatedSpace γ)

theorem EMetric.uniformEmbedding_iff' {β : Type v} {γ : Type w} [EMetricSpace γ] [EMetricSpace β] {f : γ → β} : UniformEmbedding f ↔ (∀ ε > 0, ∃ δ > 0, ∀ {a b : γ}, edist a b < δ → edist (f a) (f b) < ε) ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : γ}, edist (f a) (f b) < ε → edist a b < δ

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

@[reducible]

def EMetricSpace.ofT0PseudoEMetricSpace (α : Type u_2) [PseudoEMetricSpace α] [T0Space α] : EMetricSpace α

If a PseudoEMetricSpace is a T₀ space, then it is an EMetricSpace.

Equations

• EMetricSpace.ofT0PseudoEMetricSpace α = let src := inst✝; EMetricSpace.mk (_ : ∀ {x y : α}, edist x y = 0 → x = y)

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

Auxiliary function to replace the uniformity on an emetric space with a uniformity which is equal to the original one, but maybe not defeq. This is useful if one wants to construct an emetric space with a specified uniformity. See Note [forgetful inheritance] explaining why having definitionally the right uniformity is often important.

Equations

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

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

The extended metric induced by an injective function taking values in an emetric space.

Equations

• EMetricSpace.induced f hf m = let src := PseudoEMetricSpace.induced f EMetricSpace.toPseudoEMetricSpace; EMetricSpace.mk (_ : ∀ {x y : γ}, edist x y = 0 → x = y)

instance instEMetricSpaceSubtype {α : Type u_2} {p : α → Prop} [EMetricSpace α] : EMetricSpace (Subtype p)

EMetric space instance on subsets of emetric spaces

Equations

• instEMetricSpaceSubtype = EMetricSpace.induced Subtype.val (_ : Function.Injective fun (a : Subtype p) => ↑a) inst

instance instEMetricSpaceAddOpposite {α : Type u_2} [EMetricSpace α] : EMetricSpace αᵃᵒᵖ

EMetric space instance on the additive opposite of an emetric space.

Equations

• instEMetricSpaceAddOpposite = EMetricSpace.induced AddOpposite.unop (_ : Function.Injective AddOpposite.unop) inst

instance instEMetricSpaceMulOpposite {α : Type u_2} [EMetricSpace α] : EMetricSpace αᵐᵒᵖ

EMetric space instance on the multiplicative opposite of an emetric space.

Equations

• instEMetricSpaceMulOpposite = EMetricSpace.induced MulOpposite.unop (_ : Function.Injective MulOpposite.unop) inst

instance instEMetricSpaceULift {α : Type u_2} [EMetricSpace α] : EMetricSpace (ULift.{u_3, u_2} α)

Equations

• instEMetricSpaceULift = EMetricSpace.induced ULift.down (_ : Function.Injective ULift.down) inst

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

The product of two emetric spaces, with the max distance, is an extended metric spaces. We make sure that the uniform structure thus constructed is the one corresponding to the product of uniform spaces, to avoid diamond problems.

Equations

• Prod.emetricSpaceMax = EMetricSpace.ofT0PseudoEMetricSpace (γ × β)

theorem uniformity_edist {γ : Type w} [EMetricSpace γ] : uniformity γ = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : γ × γ | edist p.1 p.2 < ε}

Reformulation of the uniform structure in terms of the extended distance

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

The product of a finite number of emetric spaces, with the max distance, is still an emetric space. This construction would also work for infinite products, but it would not give rise to the product topology. Hence, we only formalize it in the good situation of finitely many spaces.

Equations

• emetricSpacePi = EMetricSpace.ofT0PseudoEMetricSpace ((b : β) → π b)

theorem EMetric.countable_closure_of_compact {γ : Type w} [EMetricSpace γ] {s : Set γ} (hs : IsCompact s) : ∃ t ⊆ s, Set.Countable t ∧ s = closure t

A compact set in an emetric space is separable, i.e., it is the closure of a countable set.

theorem EMetric.diam_eq_zero_iff {γ : Type w} [EMetricSpace γ] {s : Set γ} : EMetric.diam s = 0 ↔ Set.Subsingleton s

theorem EMetric.diam_pos_iff {γ : Type w} [EMetricSpace γ] {s : Set γ} : 0 < EMetric.diam s ↔ Set.Nontrivial s

theorem EMetric.diam_pos_iff' {γ : Type w} [EMetricSpace γ] {s : Set γ} : 0 < EMetric.diam s ↔ ∃ x ∈ s, ∃ y ∈ s, x ≠ y

Separation quotient

instance instEDistSeparationQuotientToUniformSpace {X : Type u_1} [PseudoEMetricSpace X] : EDist (UniformSpace.SeparationQuotient X)

Equations

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

@[simp]

theorem UniformSpace.SeparationQuotient.edist_mk {X : Type u_1} [PseudoEMetricSpace X] (x : X) (y : X) : edist (Quot.mk Setoid.r x) (Quot.mk Setoid.r y) = edist x y

instance instEMetricSpaceSeparationQuotientToUniformSpace {X : Type u_1} [PseudoEMetricSpace X] : EMetricSpace (UniformSpace.SeparationQuotient X)

Equations

• instEMetricSpaceSeparationQuotientToUniformSpace = EMetricSpace.ofT0PseudoEMetricSpace (UniformSpace.SeparationQuotient X)

Additive, Multiplicative

The distance on those type synonyms is inherited without change.

instance instEDistAdditive {X : Type u_1} [EDist X] : EDist (Additive X)

Equations

• instEDistAdditive = inst

instance instEDistMultiplicative {X : Type u_1} [EDist X] : EDist (Multiplicative X)

Equations

• instEDistMultiplicative = inst

@[simp]

theorem edist_ofMul {X : Type u_1} [EDist X] (a : X) (b : X) : edist (Additive.ofMul a) (Additive.ofMul b) = edist a b

@[simp]

theorem edist_ofAdd {X : Type u_1} [EDist X] (a : X) (b : X) : edist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = edist a b

@[simp]

theorem edist_toMul {X : Type u_1} [EDist X] (a : Additive X) (b : Additive X) : edist (Additive.toMul a) (Additive.toMul b) = edist a b

@[simp]

theorem edist_toAdd {X : Type u_1} [EDist X] (a : Multiplicative X) (b : Multiplicative X) : edist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = edist a b

instance instPseudoEMetricSpaceAdditive {X : Type u_1} [PseudoEMetricSpace X] : PseudoEMetricSpace (Additive X)

Equations

• instPseudoEMetricSpaceAdditive = inst

instance instPseudoEMetricSpaceMultiplicative {X : Type u_1} [PseudoEMetricSpace X] : PseudoEMetricSpace (Multiplicative X)

Equations

• instPseudoEMetricSpaceMultiplicative = inst

instance instEMetricSpaceAdditive {X : Type u_1} [EMetricSpace X] : EMetricSpace (Additive X)

Equations

• instEMetricSpaceAdditive = inst

instance instEMetricSpaceMultiplicative {X : Type u_1} [EMetricSpace X] : EMetricSpace (Multiplicative X)

Equations

• instEMetricSpaceMultiplicative = inst

Order dual

The distance on this type synonym is inherited without change.

instance instEDistOrderDual {X : Type u_1} [EDist X] : EDist Xᵒᵈ

Equations

• instEDistOrderDual = inst

@[simp]

theorem edist_toDual {X : Type u_1} [EDist X] (a : X) (b : X) : edist (OrderDual.toDual a) (OrderDual.toDual b) = edist a b

@[simp]

theorem edist_ofDual {X : Type u_1} [EDist X] (a : Xᵒᵈ) (b : Xᵒᵈ) : edist (OrderDual.ofDual a) (OrderDual.ofDual b) = edist a b

instance instPseudoEMetricSpaceOrderDual {X : Type u_1} [PseudoEMetricSpace X] : PseudoEMetricSpace Xᵒᵈ

Equations

• instPseudoEMetricSpaceOrderDual = inst

instance instEMetricSpaceOrderDual {X : Type u_1} [EMetricSpace X] : EMetricSpace Xᵒᵈ

Equations

• instEMetricSpaceOrderDual = inst