Lemmas around weak (pseudo) extended metric spaces.

In this file we show that whenever some : α → Option α is an open embedding and α is a WeakPseudoEMetricSpace, then Option α is as well in a natural manner. We then use this to prove ℝ≥0 and EReal are weak extended metric spaces.

Main statements

• Option.weakPseudoEMetricSpace_of_isOpenEmbedding: states that under a weak condition, if α is a weak pseudo extended space, so is Option α.
• instWeakPseudoEMetricSpaceOnePoint: The one point compactification of a weak pseudo extended metric space is a weak pseudo extended metric space.
• instWeakEMetricSpaceENNReal: ℝ≥0∞ is a weak extended metric space.
• instWeakEMetricSpaceEReal: EReal is a weak extended metric space.

TODO: Some lemmas around order topologies can likely be generalised from linear orders to pre- or partial orders.

@[instance_reducible, instance 100]

instance Option.toEDist {α : Type u} [EDist α] : EDist (Option α)

Given some (extended) distance function on α, it can be extended to a distance function on Option α by defining edist none a = 0 if a = none and ∞ otherwise.

Equations

• Option.toEDist = { edist := fun (x x_1 : Option α) => match x, x_1 with | none, some x => ⊤ | none, none => 0 | some x, none => ⊤ | some x, some y => edist x y }

@[simp]

theorem Option.edist_none_none {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] : edist none none = 0

@[simp]

theorem Option.edist_none_some {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {a : α} : edist none (some a) = ⊤

@[simp]

theorem Option.edist_some_none {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {a : α} : edist (some a) none = ⊤

@[simp]

theorem Option.edist_some_some {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {a b : α} : edist (some a) (some b) = edist a b

theorem Option.some_eball {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] (a : α) (r : ENNReal) : some '' Metric.eball a r = Metric.eball (some a) r

theorem Option.edist_self' {α : Type u} [TopologicalSpace α] (m : WeakPseudoEMetricSpace α) (x : Option α) : edist x x = 0

theorem Option.edist_comm' {α : Type u} [TopologicalSpace α] (m : WeakPseudoEMetricSpace α) (x y : Option α) : edist x y = edist y x

theorem Option.edist_triangle' {α : Type u} [TopologicalSpace α] (m : WeakPseudoEMetricSpace α) (x y z : Option α) : edist x z ≤ edist x y + edist y z

theorem Option.ball_infty_of_pos {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {r : ENNReal} (hr : 0 < r) : Metric.eball none r = {none}

@[reducible, inline]

abbrev Option.WeakPseudoEMetricSpace.OfIsOpenEmbedding {α : Type u} [t : TopologicalSpace α] [TopologicalSpace (Option α)] [m : WeakPseudoEMetricSpace α] [inst : EDist (Option α)] (h_edist : inst = toEDist) (h : Topology.IsOpenEmbedding some) : WeakPseudoEMetricSpace (Option α)

If some : α → Option α is an open embedding and α is has a weak pseudo extended metric structure, the structure extends naturally to Option α.

Equations

• Option.WeakPseudoEMetricSpace.OfIsOpenEmbedding h_edist h = { toEDist := inst, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, topology_le := ⋯, topology_eq_on_restrict := ⋯ }

@[reducible, inline]

abbrev Option.WeakEMetricSpace.OfIsOpenEmbedding {α : Type u} [t : TopologicalSpace α] [TopologicalSpace (Option α)] [m : WeakEMetricSpace α] [inst : EDist (Option α)] (h_edist : inst = toEDist) (h : Topology.IsOpenEmbedding some) : WeakEMetricSpace (Option α)

If some : α → Option α is an open embedding and α is has a weak pseudo extended metric structure, the structure extends naturally to Option α.

Equations

• Option.WeakEMetricSpace.OfIsOpenEmbedding h_edist h = { toWeakPseudoEMetricSpace := Option.WeakPseudoEMetricSpace.OfIsOpenEmbedding h_edist h, eq_of_edist_eq_zero := ⋯ }

theorem WithTop.isOpenEmbedding_some {α : Type u} [t : TopologicalSpace α] [LinearOrder α] [OrderTopology α] : Topology.IsOpenEmbedding some

If α has a linear order topology, some : α → WithTop α is an open embedding with respect to the order topologies.

theorem WithBot.isOpenEmbedding_some {α : Type u} [t : TopologicalSpace α] [LinearOrder α] [OrderTopology α] : Topology.IsOpenEmbedding some

@[instance_reducible]

instance instEDistWithTop {α : Type u} [EDist α] : EDist (WithTop α)

Equations

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

@[instance_reducible]

instance instEDistWithBot {α : Type u} [EDist α] : EDist (WithBot α)

Equations

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

@[instance_reducible]

instance instWeakPseudoEMetricSpaceWithTop {α : Type u} [t : TopologicalSpace α] [LinearOrder α] [OrderTopology α] [m : WeakPseudoEMetricSpace α] : WeakPseudoEMetricSpace (WithTop α)

If α has a topology induced by a linear order and is a weak pseudo extended metric space, so is WithTop α

Equations

• instWeakPseudoEMetricSpaceWithTop = { toEDist := instEDistWithTop, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, topology_le := ⋯, topology_eq_on_restrict := ⋯ }

@[instance_reducible]

instance instWeakPseudoEMetricSpaceWithBot {α : Type u} [t : TopologicalSpace α] [LinearOrder α] [OrderTopology α] [m : WeakPseudoEMetricSpace α] : WeakPseudoEMetricSpace (WithBot α)

Equations

• instWeakPseudoEMetricSpaceWithBot = { toEDist := instEDistWithBot, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, topology_le := ⋯, topology_eq_on_restrict := ⋯ }

@[instance_reducible]

instance instWeakEMetricSpaceWithTop {α : Type u} [t : TopologicalSpace α] [LinearOrder α] [OrderTopology α] [m : WeakEMetricSpace α] : WeakEMetricSpace (WithTop α)

If α has a topology induced by a linear order and is a weak extended metric space, so is WithTop α

Equations

• instWeakEMetricSpaceWithTop = { toWeakPseudoEMetricSpace := instWeakPseudoEMetricSpaceWithTop, eq_of_edist_eq_zero := ⋯ }

@[instance_reducible]

instance instWeakEMetricSpaceWithBot {α : Type u} [t : TopologicalSpace α] [LinearOrder α] [OrderTopology α] [m : WeakEMetricSpace α] : WeakEMetricSpace (WithBot α)

Equations

• instWeakEMetricSpaceWithBot = { toWeakPseudoEMetricSpace := instWeakPseudoEMetricSpaceWithBot, eq_of_edist_eq_zero := ⋯ }

@[instance_reducible]

instance instEDistOnePoint {α : Type u} [EDist α] : EDist (OnePoint α)

Equations

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

@[instance_reducible]

instance instWeakPseudoEMetricSpaceOnePoint {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] : WeakPseudoEMetricSpace (OnePoint α)

The one point compactification of a weak pseudo extended metric space is again a weak pseudo extended metric space.

Equations

• instWeakPseudoEMetricSpaceOnePoint = { toEDist := instEDistOnePoint, edist_self := ⋯, edist_comm := ⋯, edist_triangle := ⋯, topology_le := ⋯, topology_eq_on_restrict := ⋯ }

@[instance_reducible]

instance instWeakEMetricSpaceOnePoint {α : Type u} [t : TopologicalSpace α] [m : WeakEMetricSpace α] : WeakEMetricSpace (OnePoint α)

The one point compactification of a weak extended metric space is again a weak extended metric space.

Equations

• instWeakEMetricSpaceOnePoint = { toWeakPseudoEMetricSpace := instWeakPseudoEMetricSpaceOnePoint, eq_of_edist_eq_zero := ⋯ }

@[instance_reducible]

noncomputable instance instWeakEMetricSpaceENNReal : WeakEMetricSpace ENNReal

ℝ≥0∞ is a weak extended metric space with its usual distance function.

Equations

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

@[instance_reducible]

noncomputable instance instWeakEMetricSpaceEReal : WeakEMetricSpace EReal

EReal is a weak extended metric space with its usual distance function.

Equations

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

@[instance_reducible]

noncomputable instance instWeakEMetricSpaceENat : WeakEMetricSpace ℕ∞

ℕ∞ is a weak extended metric space with its usual distance function.

Equations

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

@[simp]

theorem ENNReal.edist_top_coe (a : NNReal) : edist ⊤ ↑a = ⊤

@[simp]

theorem ENNReal.edist_coe_top (a : NNReal) : edist ↑a ⊤ = ⊤

@[simp]

theorem ENNReal.edist_coe (a b : NNReal) : edist ↑a ↑b = edist a b

@[simp]

theorem ENNReal.edist_eq_top_iff (a b : ENNReal) : edist a b = ⊤ ↔ a ≠ b ∧ (a = ⊤ ∨ b = ⊤)

theorem ENNReal.edist_eq_max (a b : ENNReal) : edist a b = max (a - b) (b - a)

theorem ENNReal.edist_le_iff_le_add_left (a b c : ENNReal) : edist a b ≤ c ↔ a ≤ c + b ∧ b ≤ c + a

theorem ENNReal.edist_le_iff_le_add_right (a b c : ENNReal) : edist a b ≤ c ↔ a ≤ b + c ∧ b ≤ a + c

theorem ENNReal.sub_le_dist (a b : ENNReal) : a - b ≤ edist a b

theorem ENNReal.le_add_edist (a b : ENNReal) : a ≤ b + edist a b

@[simp]

theorem ENNReal.edist_zero_left (a : ENNReal) : edist 0 a = a

@[simp]

theorem ENNReal.edist_zero_right (a : ENNReal) : edist a 0 = a

@[simp]

theorem ENNReal.edist_add_left (a b : ENNReal) {c : ENNReal} (hc : c ≠ ⊤) : edist (c + a) (c + b) = edist a b

@[simp]

theorem ENNReal.edist_add_right (a b : ENNReal) {c : ENNReal} (hc : c ≠ ⊤) : edist (a + c) (b + c) = edist a b

theorem ENNReal.edist_mul_left (a b : ENNReal) {c : ENNReal} (hc : c ≠ ⊤) : edist (c * a) (c * b) = c * edist a b

theorem ENNReal.edist_mul_right (a b : ENNReal) {c : ENNReal} (hc : c ≠ ⊤) : edist (a * c) (b * c) = edist a b * c