doc-next-gen

Mathlib.Topology.EMetricSpace.Defs

Module docstring

{"# 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. ","### Additive, Multiplicative

The distance on those type synonyms is inherited without change. ","### Order dual

The distance on this type synonym is inherited without change. "}

uniformity_dist_of_mem_uniformity theorem
[LT β] {U : Filter (α × α)} (z : β) (D : α → α → β) (H : ∀ s, s ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s) : U = ⨅ ε > z, 𝓟 {p : α × α | D p.1 p.2 < ε}
Full source 
/-- Characterizing uniformities associated to a (generalized) distance function `D`
in terms of the elements of the uniformity. -/
theorem uniformity_dist_of_mem_uniformity [LT β] {U : Filter (α × α)} (z : β)
    (D : α → α → β) (H : ∀ s, s ∈ Us ∈ U ↔ ∃ ε > z, ∀ {a b : α}, D a b < ε → (a, b) ∈ s) :
    U = ⨅ ε > z, 𝓟 { p : α × α | D p.1 p.2 < ε } :=
  HasBasis.eq_biInf ⟨fun s => by simp only [H, subset_def, Prod.forall, mem_setOf]⟩
Characterization of Uniformity via Distance Function
Informal description
Let $\beta$ be a type with a strict order relation $<$, and let $U$ be a filter on $\alpha \times \alpha$. Given a base point $z \in \beta$ and a distance function $D : \alpha \times \alpha \to \beta$ such that for any set $s$, $s$ belongs to $U$ if and only if there exists $\epsilon > z$ such that for all $a, b \in \alpha$, if $D(a,b) < \epsilon$ then $(a,b) \in s$. Then the uniformity $U$ can be expressed as: \[ U = \bigsqcap_{\epsilon > z} \mathcal{P}\{(x,y) \in \alpha \times \alpha \mid D(x,y) < \epsilon\} \] where $\mathcal{P}$ denotes the powerset filter and $\bigsqcap$ is the infimum of filters.
EDist structure
(α : Type*)
Full source 
/-- `EDist α` means that `α` is equipped with an extended distance. -/
@[ext]
class EDist (α : Type*) where
  /-- Extended distance between two points -/
  edist : α → α → ℝ≥0∞
Extended Distance Structure
Informal description
The structure `EDist α` represents a type `α` equipped with an extended distance function `edist : α → α → ℝ≥0∞`, where `ℝ≥0∞` denotes the extended non-negative real numbers (including infinity). This distance function satisfies the following properties: 1. Reflexivity: `edist x x = 0` for all `x ∈ α`. 2. Symmetry: `edist x y = edist y x` for all `x, y ∈ α`. 3. Triangle inequality: `edist x z ≤ edist x y + edist y z` for all `x, y, z ∈ α`.
uniformSpaceOfEDist definition
(edist : α → α → ℝ≥0∞) (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 α
Full source 
/-- Creating a uniform space from an extended distance. -/
def uniformSpaceOfEDist (edist : α → α → ℝ≥0∞) (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 α :=
  .ofFun edist edist_self edist_comm edist_triangle fun ε ε0 =>
    ⟨ε / 2, ENNReal.half_pos ε0.ne', fun _ h₁ _ h₂ =>
      (ENNReal.add_lt_add h₁ h₂).trans_eq (ENNReal.add_halves _)⟩
Uniform space construction from an extended distance function
Informal description
Given a type $\alpha$ and a function $\text{edist} : \alpha \times \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ satisfying: 1. Reflexivity: $\text{edist}(x, x) = 0$ for all $x \in \alpha$, 2. Symmetry: $\text{edist}(x, y) = \text{edist}(y, x)$ for all $x, y \in \alpha$, 3. Triangle inequality: $\text{edist}(x, z) \leq \text{edist}(x, y) + \text{edist}(y, z)$ for all $x, y, z \in \alpha$, the function constructs a uniform space structure on $\alpha$ where the uniformity is generated by the sets $\{(x, y) \mid \text{edist}(x, y) < \varepsilon\}$ for $\varepsilon > 0$.
PseudoEMetricSpace structure
(α : Type u) : Type u extends EDist α
Full source 
/-- A pseudo extended metric space is a type endowed with a `ℝ≥0∞`-valued distance `edist`
satisfying reflexivity `edist x x = 0`, commutativity `edist x y = edist y x`, and the triangle
inequality `edist x z ≤ edist x y + edist y z`.

Note that we do not require `edist x y = 0 → x = y`. See extended metric spaces (`EMetricSpace`) for
the similar class with that stronger assumption.

Any pseudo extended metric space is a topological space and a uniform space (see `TopologicalSpace`,
`UniformSpace`), where the topology and uniformity come from the metric.
Note that a T1 pseudo extended metric space is just an extended metric space.

We make the uniformity/topology part of the data instead of deriving it from the metric. This eg
ensures that we do not get a diamond when doing
`[PseudoEMetricSpace α] [PseudoEMetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance]. -/
class PseudoEMetricSpace (α : Type u) : Type u extends EDist α  where
  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 α := uniformSpaceOfEDist edist edist_self edist_comm edist_triangle
  uniformity_edist : 𝓤 α = ⨅ ε > 0, 𝓟 { p : α × α | edist p.1 p.2 < ε } := by rfl
Pseudo Extended Metric Space
Informal description
A pseudo extended metric space is a type $\alpha$ equipped with an extended distance function $\text{edist} : \alpha \times \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ satisfying the following properties: 1. Reflexivity: $\text{edist}(x, x) = 0$ for all $x \in \alpha$. 2. Symmetry: $\text{edist}(x, y) = \text{edist}(y, x)$ for all $x, y \in \alpha$. 3. Triangle inequality: $\text{edist}(x, z) \leq \text{edist}(x, y) + \text{edist}(y, z)$ for all $x, y, z \in \alpha$. Unlike an extended metric space, a pseudo extended metric space does not require that $\text{edist}(x, y) = 0$ implies $x = y$. Any pseudo extended metric space naturally induces a topology and a uniform structure on $\alpha$.
PseudoEMetricSpace.ext theorem
{α : Type*} {m m' : PseudoEMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m'
Full source 
/-- Two pseudo emetric space structures with the same edistance function coincide. -/
@[ext]
protected theorem PseudoEMetricSpace.ext {α : Type*} {m m' : PseudoEMetricSpace α}
    (h : m.toEDist = m'.toEDist) : m = m' := by
  obtain ⟨_, _, _, U, hU⟩ := m; rename EDist α => ed
  obtain ⟨_, _, _, U', hU'⟩ := m'; rename EDist α => ed'
  congr 1
  exact UniformSpace.ext (((show ed = ed' from h) ▸ hU).trans hU'.symm)
Uniqueness of Pseudo Extended Metric Space Structure via Extended Distance
Informal description
Let $\alpha$ be a type, and let $m$ and $m'$ be two pseudo extended metric space structures on $\alpha$. If the extended distance functions of $m$ and $m'$ coincide, i.e., $m.\text{toEDist} = m'.\text{toEDist}$, then $m = m'$.
edist_triangle_left theorem
(x y z : α) : edist x y ≤ edist z x + edist z y
Full source 
/-- Triangle inequality for the extended distance -/
theorem edist_triangle_left (x y z : α) : edist x y ≤ edist z x + edist z y := by
  rw [edist_comm z]; apply edist_triangle
Left Triangle Inequality for Extended Distance
Informal description
For any three points $x, y, z$ in a pseudo extended metric space $\alpha$, the extended distance between $x$ and $y$ satisfies the triangle inequality: \[ \text{edist}(x, y) \leq \text{edist}(z, x) + \text{edist}(z, y). \]
edist_triangle_right theorem
(x y z : α) : edist x y ≤ edist x z + edist y z
Full source 
theorem edist_triangle_right (x y z : α) : edist x y ≤ edist x z + edist y z := by
  rw [edist_comm y]; apply edist_triangle
Triangle Inequality for Extended Distance (Right Form)
Informal description
For any three points $x, y, z$ in a pseudo extended metric space $\alpha$, the extended distance between $x$ and $y$ is less than or equal to the sum of the extended distances from $x$ to $z$ and from $y$ to $z$, i.e., \[ \text{edist}(x, y) \leq \text{edist}(x, z) + \text{edist}(y, z). \]
edist_congr_right theorem
{x y z : α} (h : edist x y = 0) : edist x z = edist y z
Full source 
theorem edist_congr_right {x y z : α} (h : edist x y = 0) : edist x z = edist y z := by
  apply le_antisymm
  · rw [← zero_add (edist y z), ← h]
    apply edist_triangle
  · rw [edist_comm] at h
    rw [← zero_add (edist x z), ← h]
    apply edist_triangle
Right Congruence of Extended Distance When $\text{edist}(x,y) = 0$
Informal description
Let $x, y, z$ be points in a pseudo extended metric space $\alpha$. If the extended distance between $x$ and $y$ is zero ($\text{edist}(x,y) = 0$), then for any point $z$, the extended distances $\text{edist}(x,z)$ and $\text{edist}(y,z)$ are equal.
edist_congr_left theorem
{x y z : α} (h : edist x y = 0) : edist z x = edist z y
Full source 
theorem edist_congr_left {x y z : α} (h : edist x y = 0) : edist z x = edist z y := by
  rw [edist_comm z x, edist_comm z y]
  apply edist_congr_right h
Left Congruence of Extended Distance When $\text{edist}(x,y) = 0$
Informal description
Let $x, y, z$ be points in a pseudo extended metric space $\alpha$. If the extended distance between $x$ and $y$ is zero ($\text{edist}(x,y) = 0$), then for any point $z$, the extended distances $\text{edist}(z,x)$ and $\text{edist}(z,y)$ are equal.
edist_congr theorem
{w x y z : α} (hl : edist w x = 0) (hr : edist y z = 0) : edist w y = edist x z
Full source 
theorem edist_congr {w x y z : α} (hl : edist w x = 0) (hr : edist y z = 0) :
    edist w y = edist x z :=
  (edist_congr_right hl).trans (edist_congr_left hr)
Congruence of Extended Distance Under Zero-Distance Pairs
Informal description
Let $w, x, y, z$ be points in a pseudo extended metric space $\alpha$. If the extended distance between $w$ and $x$ is zero ($\text{edist}(w,x) = 0$) and the extended distance between $y$ and $z$ is zero ($\text{edist}(y,z) = 0$), then the extended distances $\text{edist}(w,y)$ and $\text{edist}(x,z)$ are equal.
edist_triangle4 theorem
(x y z t : α) : edist x t ≤ edist x y + edist y z + edist z t
Full source 
theorem edist_triangle4 (x y z t : α) : edist x t ≤ edist x y + edist y z + edist z t :=
  calc
    edist x t ≤ edist x z + edist z t := edist_triangle x z t
    _ ≤ edist x y + edist y z + edist z t := add_le_add_right (edist_triangle x y z) _
Extended Quadrilateral Inequality in Pseudo Extended Metric Spaces
Informal description
For any four points $x, y, z, t$ in a pseudo extended metric space $\alpha$, the extended distance from $x$ to $t$ satisfies the inequality: \[ \text{edist}(x, t) \leq \text{edist}(x, y) + \text{edist}(y, z) + \text{edist}(z, t). \]
uniformity_pseudoedist theorem
: 𝓤 α = ⨅ ε > 0, 𝓟 {p : α × α | edist p.1 p.2 < ε}
Full source 
/-- Reformulation of the uniform structure in terms of the extended distance -/
theorem uniformity_pseudoedist : 𝓤 α = ⨅ ε > 0, 𝓟 { p : α × α | edist p.1 p.2 < ε } :=
  PseudoEMetricSpace.uniformity_edist
Uniformity Filter Characterization via Extended Distance
Informal description
The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudo extended metric space $\alpha$ is equal to the infimum over all positive extended real numbers $\varepsilon$ of the principal filters generated by the sets $\{(x, y) \mid \text{edist}(x, y) < \varepsilon\}$. In other words: \[ \mathfrak{U}(\alpha) = \bigsqcap_{\varepsilon > 0} \mathcal{P}\{(x, y) \mid \text{edist}(x, y) < \varepsilon\}. \]
uniformSpace_edist theorem
: ‹PseudoEMetricSpace α›.toUniformSpace = uniformSpaceOfEDist edist edist_self edist_comm edist_triangle
Full source 
theorem uniformSpace_edist :
    ‹PseudoEMetricSpace α›.toUniformSpace =
      uniformSpaceOfEDist edist edist_self edist_comm edist_triangle :=
  UniformSpace.ext uniformity_pseudoedist
Equality of Uniform Space Structures Induced by Extended Distance
Informal description
For any pseudo extended metric space $\alpha$ with extended distance function $\text{edist}$, the uniform space structure induced by $\alpha$ is equal to the uniform space constructed from $\text{edist}$ using the properties: 1. $\text{edist}(x, x) = 0$ for all $x \in \alpha$, 2. $\text{edist}(x, y) = \text{edist}(y, x)$ for all $x, y \in \alpha$, 3. $\text{edist}(x, z) \leq \text{edist}(x, y) + \text{edist}(y, z)$ for all $x, y, z \in \alpha$.
uniformity_basis_edist theorem
: (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => {p : α × α | edist p.1 p.2 < ε}
Full source 
theorem uniformity_basis_edist :
    (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => { p : α × α | edist p.1 p.2 < ε } :=
  (@uniformSpace_edist α _).symm ▸ UniformSpace.hasBasis_ofFun ⟨1, one_pos⟩ _ _ _ _ _
Basis for Uniformity Filter via Extended Distance
Informal description
The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudo extended metric space $\alpha$ has a basis consisting of the sets $\{(x, y) \mid \text{edist}(x, y) < \varepsilon\}$ for all $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
mem_uniformity_edist theorem
{s : Set (α × α)} : s ∈ 𝓤 α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s
Full source 
/-- Characterization of the elements of the uniformity in terms of the extended distance -/
theorem mem_uniformity_edist {s : Set (α × α)} :
    s ∈ 𝓤 αs ∈ 𝓤 α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s :=
  uniformity_basis_edist.mem_uniformity_iff
Characterization of Uniformity Membership via Extended Distance
Informal description
For any set $s \subseteq \alpha \times \alpha$ in a pseudo extended metric space $\alpha$, $s$ belongs to the uniformity filter $\mathfrak{U}(\alpha)$ if and only if there exists $\varepsilon > 0$ such that for all $a, b \in \alpha$, if the extended distance $\text{edist}(a, b) < \varepsilon$, then $(a, b) \in s$.
EMetric.mk_uniformity_basis theorem
{β : Type*} {p : β → Prop} {f : β → ℝ≥0∞} (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x, p x ∧ f x ≤ ε) : (𝓤 α).HasBasis p fun x => {p : α × α | edist p.1 p.2 < f x}
Full source 
/-- 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`. -/
protected theorem EMetric.mk_uniformity_basis {β : Type*} {p : β → Prop} {f : β → ℝ≥0∞}
    (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x, p x ∧ f x ≤ ε) :
    (𝓤 α).HasBasis p fun x => { p : α × α | edist p.1 p.2 < f x } := by
  refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩
  constructor
  · rintro ⟨ε, ε₀, hε⟩
    rcases hf ε ε₀ with ⟨i, hi, H⟩
    exact ⟨i, hi, fun x hx => hε <| lt_of_lt_of_le hx.out H⟩
  · exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, H⟩
Basis Construction for Uniformity Filter via Extended Distance Function
Informal description
Let $\alpha$ be a pseudo extended metric space, $\beta$ be a type, and $p : \beta \to \text{Prop}$ be a predicate on $\beta$. Given a function $f : \beta \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that: 1. For all $x \in \beta$, if $p(x)$ holds then $f(x) > 0$. 2. For all $\varepsilon > 0$, there exists $x \in \beta$ such that $p(x)$ holds and $f(x) \leq \varepsilon$. Then the uniformity filter $\mathfrak{U}(\alpha)$ has a basis consisting of the sets $\{(a, b) \in \alpha \times \alpha \mid \text{edist}(a, b) < f(x)\}$ for all $x \in \beta$ satisfying $p(x)$.
EMetric.mk_uniformity_basis_le theorem
{β : Type*} {p : β → Prop} {f : β → ℝ≥0∞} (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x, p x ∧ f x ≤ ε) : (𝓤 α).HasBasis p fun x => {p : α × α | edist p.1 p.2 ≤ f x}
Full source 
/-- 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'`. -/
protected theorem EMetric.mk_uniformity_basis_le {β : Type*} {p : β → Prop} {f : β → ℝ≥0∞}
    (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x, p x ∧ f x ≤ ε) :
    (𝓤 α).HasBasis p fun x => { p : α × α | edist p.1 p.2 ≤ f x } := by
  refine ⟨fun s => uniformity_basis_edist.mem_iff.trans ?_⟩
  constructor
  · rintro ⟨ε, ε₀, hε⟩
    rcases exists_between ε₀ with ⟨ε', hε'⟩
    rcases hf ε' hε'.1 with ⟨i, hi, H⟩
    exact ⟨i, hi, fun x hx => hε <| lt_of_le_of_lt (le_trans hx.out H) hε'.2⟩
  · exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x hx => H (le_of_lt hx.out)⟩
Basis Construction for Uniformity Filter via Extended Distance Bounds
Informal description
Let $\alpha$ be a pseudo extended metric space. Given a type $\beta$, a predicate $p : \beta \to \text{Prop}$, and a function $f : \beta \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that: 1. For every $x \in \beta$ with $p(x)$, we have $f(x) > 0$. 2. For every $\varepsilon > 0$, there exists $x \in \beta$ with $p(x)$ and $f(x) \leq \varepsilon$. Then the uniformity filter $\mathfrak{U}(\alpha)$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{edist}(x, y) \leq f(x)\}$ for all $x \in \beta$ satisfying $p(x)$.
uniformity_basis_edist_le theorem
: (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => {p : α × α | edist p.1 p.2 ≤ ε}
Full source 
theorem uniformity_basis_edist_le :
    (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => { p : α × α | edist p.1 p.2 ≤ ε } :=
  EMetric.mk_uniformity_basis_le (fun _ => id) fun ε ε₀ => ⟨ε, ε₀, le_refl ε⟩
Basis for Uniformity Filter via Extended Distance Bounds
Informal description
The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudo extended metric space $\alpha$ has a basis consisting of all sets of the form $\{(x, y) \in \alpha \times \alpha \mid \text{edist}(x, y) \leq \varepsilon\}$ for $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
uniformity_basis_edist' theorem
(ε' : ℝ≥0∞) (hε' : 0 < ε') : (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => ε ∈ Ioo 0 ε') fun ε => {p : α × α | edist p.1 p.2 < ε}
Full source 
theorem uniformity_basis_edist' (ε' : ℝ≥0∞) (hε' : 0 < ε') :
    (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => ε ∈ Ioo 0 ε') fun ε => { p : α × α | edist p.1 p.2 < ε } :=
  EMetric.mk_uniformity_basis (fun _ => And.left) fun ε ε₀ =>
    let ⟨δ, hδ⟩ := exists_between hε'
    ⟨min ε δ, ⟨lt_min ε₀ hδ.1, lt_of_le_of_lt (min_le_right _ _) hδ.2⟩, min_le_left _ _⟩
Basis for Uniformity Filter via Extended Distance on Open Interval $(0, \varepsilon')$
Informal description
For any extended nonnegative real number $\varepsilon' > 0$, the uniformity filter $\mathfrak{U}(\alpha)$ of a pseudo extended metric space $\alpha$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{edist}(x, y) < \varepsilon\}$ for all $\varepsilon$ in the open interval $(0, \varepsilon')$.
uniformity_basis_edist_le' theorem
(ε' : ℝ≥0∞) (hε' : 0 < ε') : (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => ε ∈ Ioo 0 ε') fun ε => {p : α × α | edist p.1 p.2 ≤ ε}
Full source 
theorem uniformity_basis_edist_le' (ε' : ℝ≥0∞) (hε' : 0 < ε') :
    (𝓤 α).HasBasis (fun ε : ℝ≥0∞ => ε ∈ Ioo 0 ε') fun ε => { p : α × α | edist p.1 p.2 ≤ ε } :=
  EMetric.mk_uniformity_basis_le (fun _ => And.left) fun ε ε₀ =>
    let ⟨δ, hδ⟩ := exists_between hε'
    ⟨min ε δ, ⟨lt_min ε₀ hδ.1, lt_of_le_of_lt (min_le_right _ _) hδ.2⟩, min_le_left _ _⟩
Uniformity Basis via Extended Distance Bounds on $(0, \varepsilon')$
Informal description
For any extended nonnegative real number $\varepsilon' > 0$, the uniformity filter $\mathfrak{U}(\alpha)$ of a pseudo extended metric space $\alpha$ has a basis consisting of sets of the form $\{(x, y) \in \alpha \times \alpha \mid \text{edist}(x, y) \leq \varepsilon\}$ for all $\varepsilon$ in the open interval $(0, \varepsilon')$.
uniformity_basis_edist_nnreal theorem
: (𝓤 α).HasBasis (fun ε : ℝ≥0 => 0 < ε) fun ε => {p : α × α | edist p.1 p.2 < ε}
Full source 
theorem uniformity_basis_edist_nnreal :
    (𝓤 α).HasBasis (fun ε : ℝ≥0 => 0 < ε) fun ε => { p : α × α | edist p.1 p.2 < ε } :=
  EMetric.mk_uniformity_basis (fun _ => ENNReal.coe_pos.2) fun _ε ε₀ =>
    let ⟨δ, hδ⟩ := ENNReal.lt_iff_exists_nnreal_btwn.1 ε₀
    ⟨δ, ENNReal.coe_pos.1 hδ.1, le_of_lt hδ.2⟩
Basis for Uniformity Filter via Extended Distance with Positive Real Radii
Informal description
The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudo extended metric space $\alpha$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{edist}(x, y) < \varepsilon\}$ for all positive real numbers $\varepsilon \in \mathbb{R}_{\geq 0}$.
uniformity_basis_edist_nnreal_le theorem
: (𝓤 α).HasBasis (fun ε : ℝ≥0 => 0 < ε) fun ε => {p : α × α | edist p.1 p.2 ≤ ε}
Full source 
theorem uniformity_basis_edist_nnreal_le :
    (𝓤 α).HasBasis (fun ε : ℝ≥0 => 0 < ε) fun ε => { p : α × α | edist p.1 p.2 ≤ ε } :=
  EMetric.mk_uniformity_basis_le (fun _ => ENNReal.coe_pos.2) fun _ε ε₀ =>
    let ⟨δ, hδ⟩ := ENNReal.lt_iff_exists_nnreal_btwn.1 ε₀
    ⟨δ, ENNReal.coe_pos.1 hδ.1, le_of_lt hδ.2⟩
Basis for Uniformity Filter via Extended Distance Bounds with Nonnegative Reals
Informal description
For a pseudo extended metric space $\alpha$, the uniformity filter $\mathfrak{U}(\alpha)$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{edist}(x, y) \leq \varepsilon\}$ for all positive real numbers $\varepsilon \in \mathbb{R}_{\geq 0}$.
uniformity_basis_edist_inv_nat theorem
: (𝓤 α).HasBasis (fun _ => True) fun n : ℕ => {p : α × α | edist p.1 p.2 < (↑n)⁻¹}
Full source 
theorem uniformity_basis_edist_inv_nat :
    (𝓤 α).HasBasis (fun _ => True) fun n : ℕ => { p : α × α | edist p.1 p.2 < (↑n)⁻¹ } :=
  EMetric.mk_uniformity_basis (fun n _ ↦ ENNReal.inv_pos.2 <| ENNReal.natCast_ne_top n) fun _ε ε₀ ↦
    let ⟨n, hn⟩ := ENNReal.exists_inv_nat_lt (ne_of_gt ε₀)
    ⟨n, trivial, le_of_lt hn⟩
Basis for Uniformity Filter via Inverse Natural Numbers in Pseudo Extended Metric Spaces
Informal description
The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudo extended metric space $\alpha$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{edist}(x, y) < n^{-1}\}$ for all natural numbers $n \in \mathbb{N}$, where $n^{-1}$ denotes the multiplicative inverse of $n$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
uniformity_basis_edist_inv_two_pow theorem
: (𝓤 α).HasBasis (fun _ => True) fun n : ℕ => {p : α × α | edist p.1 p.2 < 2⁻¹ ^ n}
Full source 
theorem uniformity_basis_edist_inv_two_pow :
    (𝓤 α).HasBasis (fun _ => True) fun n : ℕ => { p : α × α | edist p.1 p.2 < 2⁻¹ ^ n } :=
  EMetric.mk_uniformity_basis (fun _ _ ↦ ENNReal.pow_pos (ENNReal.inv_pos.2 ENNReal.ofNat_ne_top) _)
    fun _ε ε₀ ↦
    let ⟨n, hn⟩ := ENNReal.exists_inv_two_pow_lt (ne_of_gt ε₀)
    ⟨n, trivial, le_of_lt hn⟩
Basis for Uniformity Filter via Powers of Half in Extended Metric Spaces
Informal description
The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudo extended metric space $\alpha$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{edist}(x, y) < 2^{-n}\}$ for all natural numbers $n$.
edist_mem_uniformity theorem
{ε : ℝ≥0∞} (ε0 : 0 < ε) : {p : α × α | edist p.1 p.2 < ε} ∈ 𝓤 α
Full source 
/-- Fixed size neighborhoods of the diagonal belong to the uniform structure -/
theorem edist_mem_uniformity {ε : ℝ≥0∞} (ε0 : 0 < ε) : { p : α × α | edist p.1 p.2 < ε }{ p : α × α | edist p.1 p.2 < ε } ∈ 𝓤 α :=
  mem_uniformity_edist.2 ⟨ε, ε0, id⟩
Neighborhoods of the Diagonal in Uniformity via Extended Distance
Informal description
For any positive extended real number $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the set $\{(a, b) \in \alpha \times \alpha \mid \text{edist}(a, b) < \varepsilon\}$ belongs to the uniformity filter $\mathfrak{U}(\alpha)$ of the pseudo extended metric space $\alpha$.
EMetric.uniformContinuousOn_iff theorem
[PseudoEMetricSpace β] {f : α → β} {s : Set α} : UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a}, a ∈ s → ∀ {b}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
Full source 
/-- ε-δ characterization of uniform continuity on a set for pseudoemetric spaces -/
theorem uniformContinuousOn_iff [PseudoEMetricSpace β] {f : α → β} {s : Set α} :
    UniformContinuousOnUniformContinuousOn f s ↔
      ∀ ε > 0, ∃ δ > 0, ∀ {a}, a ∈ s → ∀ {b}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε :=
  uniformity_basis_edist.uniformContinuousOn_iff uniformity_basis_edist
$\varepsilon$-$\delta$ Criterion for Uniform Continuity on Subsets in Pseudo Extended Metric Spaces
Informal description
Let $\alpha$ and $\beta$ be pseudo extended metric spaces. A function $f \colon \alpha \to \beta$ is uniformly continuous on a subset $s \subseteq \alpha$ if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists $\delta > 0$ such that for all $a, b \in s$, if the extended distance $\text{edist}(a, b) < \delta$, then $\text{edist}(f(a), f(b)) < \varepsilon$.
EMetric.uniformContinuous_iff theorem
[PseudoEMetricSpace β] {f : α → β} : UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε
Full source 
/-- ε-δ characterization of uniform continuity on pseudoemetric spaces -/
theorem uniformContinuous_iff [PseudoEMetricSpace β] {f : α → β} :
    UniformContinuousUniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ {a b : α}, edist a b < δ → edist (f a) (f b) < ε :=
  uniformity_basis_edist.uniformContinuous_iff uniformity_basis_edist
$\varepsilon$-$\delta$ Criterion for Uniform Continuity in Pseudo Extended Metric Spaces
Informal description
Let $\alpha$ and $\beta$ be pseudo extended metric spaces. A function $f \colon \alpha \to \beta$ is uniformly continuous if and only if for every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $a, b \in \alpha$ with $\text{edist}(a, b) < \delta$, we have $\text{edist}(f(a), f(b)) < \varepsilon$.
PseudoEMetricSpace.replaceUniformity abbrev
{α} [U : UniformSpace α] (m : PseudoEMetricSpace α) (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : PseudoEMetricSpace α
Full source 
/-- 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.
See note [reducible non-instances].
-/
abbrev PseudoEMetricSpace.replaceUniformity {α} [U : UniformSpace α] (m : PseudoEMetricSpace α)
    (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : PseudoEMetricSpace α where
  edist := @edist _ m.toEDist
  edist_self := edist_self
  edist_comm := edist_comm
  edist_triangle := edist_triangle
  toUniformSpace := U
  uniformity_edist := H.trans (@PseudoEMetricSpace.uniformity_edist α _)
Construction of Pseudo Extended Metric Space from Uniformity Condition
Informal description
Given a uniform space $\alpha$ with uniformity $\mathfrak{U}(\alpha)$ and a pseudo extended metric space structure $m$ on $\alpha$, if the uniformity $\mathfrak{U}(\alpha)$ coincides with the uniformity induced by $m$, then $m$ defines a valid pseudo extended metric space structure on $\alpha$.
PseudoEMetricSpace.induced abbrev
{α β} (f : α → β) (m : PseudoEMetricSpace β) : PseudoEMetricSpace α
Full source 
/-- The extended pseudometric induced by a function taking values in a pseudoemetric space.
See note [reducible non-instances]. -/
abbrev PseudoEMetricSpace.induced {α β} (f : α → β) (m : PseudoEMetricSpace β) :
    PseudoEMetricSpace α where
  edist x y := edist (f x) (f y)
  edist_self _ := edist_self _
  edist_comm _ _ := edist_comm _ _
  edist_triangle _ _ _ := edist_triangle _ _ _
  toUniformSpace := UniformSpace.comap f m.toUniformSpace
  uniformity_edist := (uniformity_basis_edist.comap (Prod.map f f)).eq_biInf
Induced Pseudo Extended Metric Space via Function
Informal description
Given a function $f \colon \alpha \to \beta$ and a pseudo extended metric space structure on $\beta$, the induced pseudo extended metric space structure on $\alpha$ is defined by setting the extended distance between any two points $x, y \in \alpha$ to be $\text{edist}(f(x), f(y))$.
instPseudoEMetricSpaceSubtype instance
{α : Type*} {p : α → Prop} [PseudoEMetricSpace α] : PseudoEMetricSpace (Subtype p)
Full source 
/-- Pseudoemetric space instance on subsets of pseudoemetric spaces -/
instance {α : Type*} {p : α → Prop} [PseudoEMetricSpace α] : PseudoEMetricSpace (Subtype p) :=
  PseudoEMetricSpace.induced Subtype.val ‹_›
Pseudo Extended Metric Space Structure on Subtypes
Informal description
For any type $\alpha$ with a pseudo extended metric space structure and any predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a pseudo extended metric space structure where the extended distance between two elements $x$ and $y$ in the subtype is equal to their extended distance in $\alpha$.
Subtype.edist_eq theorem
{p : α → Prop} (x y : Subtype p) : edist x y = edist (x : α) y
Full source 
/-- The extended pseudodistance on a subset of a pseudoemetric space is the restriction of
the original pseudodistance, by definition. -/
theorem Subtype.edist_eq {p : α → Prop} (x y : Subtype p) : edist x y = edist (x : α) y := rfl
Subtype Extended Distance Equals Ambient Space Distance
Informal description
For any subset $S = \{x \in \alpha \mid p(x)\}$ of a pseudo extended metric space $\alpha$, the extended distance between two points $x, y \in S$ is equal to their extended distance in the ambient space $\alpha$, i.e., $\text{edist}(x, y) = \text{edist}(x, y)$ where the left-hand side is computed in $S$ and the right-hand side is computed in $\alpha$.
Subtype.edist_mk_mk theorem
{p : α → Prop} {x y : α} (hx : p x) (hy : p y) : edist (⟨x, hx⟩ : Subtype p) ⟨y, hy⟩ = edist x y
Full source 
/-- The extended pseudodistance on a subtype of a pseudoemetric space is the restriction of
the original pseudodistance, by definition. -/
@[simp]
theorem Subtype.edist_mk_mk {p : α → Prop} {x y : α} (hx : p x) (hy : p y) :
    edist (⟨x, hx⟩ : Subtype p) ⟨y, hy⟩ = edist x y :=
  rfl
Extended Distance Equality in Subtype Construction
Informal description
For any pseudo extended metric space $\alpha$ and any predicate $p$ on $\alpha$, the extended distance between two elements $\langle x, hx \rangle$ and $\langle y, hy \rangle$ in the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the extended distance between $x$ and $y$ in $\alpha$, i.e., \[ \text{edist}(\langle x, hx \rangle, \langle y, hy \rangle) = \text{edist}(x, y). \]
MulOpposite.instPseudoEMetricSpace instance
{α : Type*} [PseudoEMetricSpace α] : PseudoEMetricSpace αᵐᵒᵖ
Full source 
/-- Pseudoemetric space instance on the multiplicative opposite of a pseudoemetric space. -/
@[to_additive "Pseudoemetric space instance on the additive opposite of a pseudoemetric space."]
instance {α : Type*} [PseudoEMetricSpace α] : PseudoEMetricSpace αᵐᵒᵖ :=
  PseudoEMetricSpace.induced unop ‹_›
Pseudo Extended Metric Space Structure on the Multiplicative Opposite
Informal description
For any pseudo extended metric space $\alpha$, the multiplicative opposite $\alpha^\text{op}$ inherits a pseudo extended metric space structure where the extended distance between two elements $x, y \in \alpha^\text{op}$ is equal to the extended distance between their corresponding elements in $\alpha$.
MulOpposite.edist_unop theorem
(x y : αᵐᵒᵖ) : edist (unop x) (unop y) = edist x y
Full source 
@[to_additive]
theorem edist_unop (x y : αᵐᵒᵖ) : edist (unop x) (unop y) = edist x y := rfl
Extended Distance Preservation under Multiplicative Opposite Projection
Informal description
For any elements $x, y$ in the multiplicative opposite $\alpha^\text{op}$ of a pseudo extended metric space $\alpha$, the extended distance between their projections back to $\alpha$ equals the extended distance between $x$ and $y$ in $\alpha^\text{op}$. That is, $\text{edist}(\text{unop}(x), \text{unop}(y)) = \text{edist}(x, y)$.
MulOpposite.edist_op theorem
(x y : α) : edist (op x) (op y) = edist x y
Full source 
@[to_additive]
theorem edist_op (x y : α) : edist (op x) (op y) = edist x y := rfl
Extended Distance Preservation under Multiplicative Opposite Embedding
Informal description
For any two elements $x$ and $y$ in a pseudo extended metric space $\alpha$, the extended distance between their images under the canonical embedding into the multiplicative opposite $\alpha^\text{op}$ is equal to the extended distance between $x$ and $y$ in $\alpha$. That is, $\text{edist}(\text{op}(x), \text{op}(y)) = \text{edist}(x, y)$.
instPseudoEMetricSpaceULift instance
: PseudoEMetricSpace (ULift α)
Full source 
instance : PseudoEMetricSpace (ULift α) := PseudoEMetricSpace.induced ULift.down ‹_›
Pseudo Extended Metric Space Structure on Universe-Lifted Types
Informal description
The type `ULift α` of universe-lifted elements of `α` inherits a pseudo extended metric space structure from `α`, where the extended distance between two lifted elements `x` and `y` is equal to the extended distance between their underlying elements in `α`.
ULift.edist_eq theorem
(x y : ULift α) : edist x y = edist x.down y.down
Full source 
theorem ULift.edist_eq (x y : ULift α) : edist x y = edist x.down y.down := rfl
Extended Distance Preservation under Universe Lifting
Informal description
For any two elements $x$ and $y$ in the universe-lifted type $\text{ULift}\,\alpha$, the extended distance $\text{edist}(x, y)$ is equal to the extended distance $\text{edist}(x.\text{down}, y.\text{down})$ between their underlying elements in $\alpha$.
ULift.edist_up_up theorem
(x y : α) : edist (ULift.up x) (ULift.up y) = edist x y
Full source 
@[simp]
theorem ULift.edist_up_up (x y : α) : edist (ULift.up x) (ULift.up y) = edist x y := rfl
Extended Distance Preservation under Lifting: $\text{edist}(\text{up}\,x, \text{up}\,y) = \text{edist}(x, y)$
Informal description
For any two elements $x$ and $y$ of type $\alpha$, the extended distance between their lifted versions $\text{up}\,x$ and $\text{up}\,y$ in the universe-lifted type $\text{ULift}\,\alpha$ is equal to the extended distance between $x$ and $y$ in $\alpha$. That is, $\text{edist}(\text{up}\,x, \text{up}\,y) = \text{edist}(x, y)$.
Prod.pseudoEMetricSpaceMax instance
[PseudoEMetricSpace β] : PseudoEMetricSpace (α × β)
Full source 
/-- 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. -/
instance Prod.pseudoEMetricSpaceMax [PseudoEMetricSpace β] :
  PseudoEMetricSpace (α × β) where
  edist x y := edistedist x.1 y.1 ⊔ edist x.2 y.2
  edist_self x := by simp
  edist_comm x y := by simp [edist_comm]
  edist_triangle _ _ _ :=
    max_le (le_trans (edist_triangle _ _ _) (add_le_add (le_max_left _ _) (le_max_left _ _)))
      (le_trans (edist_triangle _ _ _) (add_le_add (le_max_right _ _) (le_max_right _ _)))
  uniformity_edist := uniformity_prod.trans <| by
    simp [PseudoEMetricSpace.uniformity_edist, ← iInf_inf_eq, setOf_and]
  toUniformSpace := inferInstance
Pseudo Extended Metric Space Structure on Product Spaces via Maximum Distance
Informal description
The product $\alpha \times \beta$ of two pseudo extended metric spaces $\alpha$ and $\beta$ is naturally equipped with a pseudo extended metric space structure, where the extended distance between two points $(x_1, y_1)$ and $(x_2, y_2)$ is defined as the maximum of the extended distances $\text{edist}(x_1, x_2)$ and $\text{edist}(y_1, y_2)$. This construction ensures that the induced uniform structure on $\alpha \times \beta$ coincides with the product uniform structure.
Prod.edist_eq theorem
[PseudoEMetricSpace β] (x y : α × β) : edist x y = max (edist x.1 y.1) (edist x.2 y.2)
Full source 
theorem Prod.edist_eq [PseudoEMetricSpace β] (x y : α × β) :
    edist x y = max (edist x.1 y.1) (edist x.2 y.2) :=
  rfl
Extended Distance Formula for Product Spaces: $\text{edist}(x, y) = \max(\text{edist}(x_1, y_1), \text{edist}(x_2, y_2))$
Informal description
Let $\alpha$ and $\beta$ be pseudo extended metric spaces. For any two points $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product space $\alpha \times \beta$, the extended distance between $x$ and $y$ is given by the maximum of the extended distances between their components: \[ \text{edist}(x, y) = \max(\text{edist}(x_1, y_1), \text{edist}(x_2, y_2)). \]
EMetric.ball definition
(x : α) (ε : ℝ≥0∞) : Set α
Full source 
/-- `EMetric.ball x ε` is the set of all points `y` with `edist y x < ε` -/
def ball (x : α) (ε : ℝ≥0∞) : Set α :=
  { y | edist y x < ε }
Extended metric ball
Informal description
Given a point $x$ in a pseudo extended metric space $\alpha$ and a radius $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the extended metric ball $\text{ball}(x, \varepsilon)$ is the set of all points $y \in \alpha$ such that the extended distance $\text{edist}(y, x) < \varepsilon$.
EMetric.mem_ball theorem
: y ∈ ball x ε ↔ edist y x < ε
Full source 
@[simp] theorem mem_ball : y ∈ ball x εy ∈ ball x ε ↔ edist y x < ε := Iff.rfl
Characterization of Extended Metric Ball Membership
Informal description
For any point $y$ in a pseudo extended metric space $\alpha$, $y$ belongs to the extended metric ball centered at $x$ with radius $\varepsilon$ if and only if the extended distance from $y$ to $x$ is strictly less than $\varepsilon$. In symbols: $$ y \in \text{ball}(x, \varepsilon) \leftrightarrow \text{edist}(y, x) < \varepsilon. $$
EMetric.mem_ball' theorem
: y ∈ ball x ε ↔ edist x y < ε
Full source 
theorem mem_ball' : y ∈ ball x εy ∈ ball x ε ↔ edist x y < ε := by rw [edist_comm, mem_ball]
Symmetric Characterization of Extended Metric Ball Membership
Informal description
For any point $y$ in a pseudo extended metric space $\alpha$, $y$ belongs to the extended metric ball centered at $x$ with radius $\varepsilon$ if and only if the extended distance from $x$ to $y$ is strictly less than $\varepsilon$. In symbols: $$ y \in \text{ball}(x, \varepsilon) \leftrightarrow \text{edist}(x, y) < \varepsilon. $$
EMetric.closedBall definition
(x : α) (ε : ℝ≥0∞)
Full source 
/-- `EMetric.closedBall x ε` is the set of all points `y` with `edist y x ≤ ε` -/
def closedBall (x : α) (ε : ℝ≥0∞) :=
  { y | edist y x ≤ ε }
Closed ball in an extended metric space
Informal description
For a point $x$ in an extended metric space $\alpha$ and a nonnegative extended real number $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the closed ball $\text{closedBall}(x, \varepsilon)$ is the set of all points $y \in \alpha$ such that the extended distance $\text{edist}(y, x)$ is less than or equal to $\varepsilon$.
EMetric.mem_closedBall theorem
: y ∈ closedBall x ε ↔ edist y x ≤ ε
Full source 
@[simp] theorem mem_closedBall : y ∈ closedBall x εy ∈ closedBall x ε ↔ edist y x ≤ ε := Iff.rfl
Characterization of Closed Ball Membership in Extended Metric Spaces
Informal description
For any points $x$ and $y$ in an extended metric space $\alpha$ and any extended nonnegative real number $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the point $y$ belongs to the closed ball centered at $x$ with radius $\varepsilon$ if and only if the extended distance from $y$ to $x$ is less than or equal to $\varepsilon$, i.e., $\text{edist}(y, x) \leq \varepsilon$.
EMetric.mem_closedBall' theorem
: y ∈ closedBall x ε ↔ edist x y ≤ ε
Full source 
theorem mem_closedBall' : y ∈ closedBall x εy ∈ closedBall x ε ↔ edist x y ≤ ε := by rw [edist_comm, mem_closedBall]
Characterization of Closed Ball Membership via Symmetric Distance in Extended Metric Spaces
Informal description
For any points $x$ and $y$ in a pseudo extended metric space $\alpha$ and any extended nonnegative real number $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the point $y$ belongs to the closed ball centered at $x$ with radius $\varepsilon$ if and only if the extended distance from $x$ to $y$ is less than or equal to $\varepsilon$, i.e., $\text{edist}(x, y) \leq \varepsilon$.
EMetric.closedBall_top theorem
(x : α) : closedBall x ∞ = univ
Full source 
@[simp]
theorem closedBall_top (x : α) : closedBall x ∞ = univ :=
  eq_univ_of_forall fun _ => mem_setOf.2 le_top
Closed Ball with Infinite Radius is Universal Set
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$, the closed ball centered at $x$ with radius $\infty$ is equal to the universal set $\alpha$, i.e., $\text{closedBall}(x, \infty) = \alpha$.
EMetric.ball_subset_closedBall theorem
: ball x ε ⊆ closedBall x ε
Full source 
theorem ball_subset_closedBall : ballball x ε ⊆ closedBall x ε := fun _ h => le_of_lt h.out
Open Ball is Subset of Closed Ball in Extended Metric Space
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$ and any radius $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the open ball $\text{ball}(x, \varepsilon)$ is a subset of the closed ball $\text{closedBall}(x, \varepsilon)$. In other words, for any $y \in \alpha$, if the extended distance $\text{edist}(x, y) < \varepsilon$, then $\text{edist}(x, y) \leq \varepsilon$.
EMetric.pos_of_mem_ball theorem
(hy : y ∈ ball x ε) : 0 < ε
Full source 
theorem pos_of_mem_ball (hy : y ∈ ball x ε) : 0 < ε :=
  lt_of_le_of_lt (zero_le _) hy
Positivity of Radius in Extended Metric Ball Membership
Informal description
For any point $y$ in the extended metric ball centered at $x$ with radius $\varepsilon$ in a pseudo extended metric space, the radius $\varepsilon$ must be strictly positive, i.e., $0 < \varepsilon$.
EMetric.mem_ball_self theorem
(h : 0 < ε) : x ∈ ball x ε
Full source 
theorem mem_ball_self (h : 0 < ε) : x ∈ ball x ε := by
  rwa [mem_ball, edist_self]
Self-Membership in Extended Metric Ball
Informal description
For any point $x$ in a pseudo extended metric space and any radius $\varepsilon > 0$, the point $x$ belongs to the open ball centered at $x$ with radius $\varepsilon$, i.e., $x \in \text{ball}(x, \varepsilon)$.
EMetric.mem_closedBall_self theorem
: x ∈ closedBall x ε
Full source 
theorem mem_closedBall_self : x ∈ closedBall x ε := by
  rw [mem_closedBall, edist_self]; apply zero_le
Reflexivity of Closed Balls in Extended Metric Spaces
Informal description
For any point $x$ in a pseudo extended metric space and any extended nonnegative real number $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the point $x$ belongs to the closed ball centered at $x$ with radius $\varepsilon$, i.e., $x \in \text{closedBall}(x, \varepsilon)$.
EMetric.mem_ball_comm theorem
: x ∈ ball y ε ↔ y ∈ ball x ε
Full source 
theorem mem_ball_comm : x ∈ ball y εx ∈ ball y ε ↔ y ∈ ball x ε := by rw [mem_ball', mem_ball]
Symmetry of Extended Metric Ball Membership: $x \in B(y, \varepsilon) \leftrightarrow y \in B(x, \varepsilon)$
Informal description
For any points $x$ and $y$ in a pseudo extended metric space and any radius $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the point $x$ belongs to the open ball centered at $y$ with radius $\varepsilon$ if and only if $y$ belongs to the open ball centered at $x$ with radius $\varepsilon$. In symbols: $$ x \in B(y, \varepsilon) \leftrightarrow y \in B(x, \varepsilon). $$
EMetric.mem_closedBall_comm theorem
: x ∈ closedBall y ε ↔ y ∈ closedBall x ε
Full source 
theorem mem_closedBall_comm : x ∈ closedBall y εx ∈ closedBall y ε ↔ y ∈ closedBall x ε := by
  rw [mem_closedBall', mem_closedBall]
Symmetry of Closed Ball Membership in Extended Metric Spaces
Informal description
For any points $x$ and $y$ in a pseudo extended metric space and any extended nonnegative real number $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the point $x$ belongs to the closed ball centered at $y$ with radius $\varepsilon$ if and only if $y$ belongs to the closed ball centered at $x$ with radius $\varepsilon$. In other words, $x \in \text{closedBall}(y, \varepsilon) \leftrightarrow y \in \text{closedBall}(x, \varepsilon)$.
EMetric.ball_subset_ball theorem
(h : ε₁ ≤ ε₂) : ball x ε₁ ⊆ ball x ε₂
Full source 
@[gcongr]
theorem ball_subset_ball (h : ε₁ ≤ ε₂) : ballball x ε₁ ⊆ ball x ε₂ := fun _y (yx : _ < ε₁) =>
  lt_of_lt_of_le yx h
Monotonicity of Extended Metric Balls: $B(x, \varepsilon_1) \subseteq B(x, \varepsilon_2)$ for $\varepsilon_1 \leq \varepsilon_2$
Informal description
For any point $x$ in a pseudo extended metric space and any two radii $\varepsilon_1, \varepsilon_2 \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $\varepsilon_1 \leq \varepsilon_2$, the extended metric ball centered at $x$ with radius $\varepsilon_1$ is a subset of the extended metric ball centered at $x$ with radius $\varepsilon_2$, i.e., $B(x, \varepsilon_1) \subseteq B(x, \varepsilon_2)$.
EMetric.closedBall_subset_closedBall theorem
(h : ε₁ ≤ ε₂) : closedBall x ε₁ ⊆ closedBall x ε₂
Full source 
@[gcongr]
theorem closedBall_subset_closedBall (h : ε₁ ≤ ε₂) : closedBallclosedBall x ε₁ ⊆ closedBall x ε₂ :=
  fun _y (yx : _ ≤ ε₁) => le_trans yx h
Monotonicity of Closed Balls in Extended Metric Spaces: $\varepsilon_1 \leq \varepsilon_2 \implies \text{closedBall}(x, \varepsilon_1) \subseteq \text{closedBall}(x, \varepsilon_2)$
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$ and any two extended nonnegative real numbers $\varepsilon_1, \varepsilon_2 \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ such that $\varepsilon_1 \leq \varepsilon_2$, the closed ball centered at $x$ with radius $\varepsilon_1$ is a subset of the closed ball centered at $x$ with radius $\varepsilon_2$. In other words, if $\varepsilon_1 \leq \varepsilon_2$, then $\{ y \in \alpha \mid \text{edist}(y, x) \leq \varepsilon_1 \} \subseteq \{ y \in \alpha \mid \text{edist}(y, x) \leq \varepsilon_2 \}$.
EMetric.ball_disjoint theorem
(h : ε₁ + ε₂ ≤ edist x y) : Disjoint (ball x ε₁) (ball y ε₂)
Full source 
theorem ball_disjoint (h : ε₁ + ε₂ ≤ edist x y) : Disjoint (ball x ε₁) (ball y ε₂) :=
  Set.disjoint_left.mpr fun z h₁ h₂ =>
    (edist_triangle_left x y z).not_lt <| (ENNReal.add_lt_add h₁ h₂).trans_le h
Disjointness of Extended Metric Balls under Sum Condition: $\varepsilon_1 + \varepsilon_2 \leq \text{edist}(x,y) \implies B(x,\varepsilon_1) \cap B(y,\varepsilon_2) = \emptyset$
Informal description
For any points $x$ and $y$ in a pseudo extended metric space and any radii $\varepsilon_1, \varepsilon_2 \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $\varepsilon_1 + \varepsilon_2 \leq \text{edist}(x, y)$, then the extended metric balls $B(x, \varepsilon_1)$ and $B(y, \varepsilon_2)$ are disjoint.
EMetric.ball_subset theorem
(h : edist x y + ε₁ ≤ ε₂) (h' : edist x y ≠ ∞) : ball x ε₁ ⊆ ball y ε₂
Full source 
theorem ball_subset (h : edist x y + ε₁ ≤ ε₂) (h' : edistedist x y ≠ ∞) : ballball x ε₁ ⊆ ball y ε₂ :=
  fun z zx =>
  calc
    edist z y ≤ edist z x + edist x y := edist_triangle _ _ _
    _ = edist x y + edist z x := add_comm _ _
    _ < edist x y + ε₁ := ENNReal.add_lt_add_left h' zx
    _ ≤ ε₂ := h
Inclusion of Extended Metric Balls under Distance and Radius Conditions
Informal description
Let $\alpha$ be a pseudo extended metric space with extended distance function $\text{edist}$. For any points $x, y \in \alpha$ and radii $\varepsilon_1, \varepsilon_2 \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $\text{edist}(x, y) + \varepsilon_1 \leq \varepsilon_2$ and $\text{edist}(x, y) \neq \infty$, then the extended metric ball centered at $x$ with radius $\varepsilon_1$ is contained in the extended metric ball centered at $y$ with radius $\varepsilon_2$, i.e., \[ B(x, \varepsilon_1) \subseteq B(y, \varepsilon_2). \]
EMetric.exists_ball_subset_ball theorem
(h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε
Full source 
theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε := by
  have : 0 < ε - edist y x := by simpa using h
  refine ⟨ε - edist y x, this, ball_subset ?_ (ne_top_of_lt h)⟩
  exact (add_tsub_cancel_of_le (mem_ball.mp h).le).le
Existence of Nested Extended Metric Balls: $y \in B(x,\varepsilon) \implies \exists \varepsilon'>0, B(y,\varepsilon') \subseteq B(x,\varepsilon)$
Informal description
For any points $x$ and $y$ in a pseudo extended metric space $\alpha$ and any radius $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if $y$ belongs to the extended metric ball centered at $x$ with radius $\varepsilon$, then there exists a positive radius $\varepsilon' > 0$ such that the extended metric ball centered at $y$ with radius $\varepsilon'$ is contained in the extended metric ball centered at $x$ with radius $\varepsilon$.
EMetric.ball_eq_empty_iff theorem
: ball x ε = ∅ ↔ ε = 0
Full source 
theorem ball_eq_empty_iff : ballball x ε = ∅ ↔ ε = 0 :=
  eq_empty_iff_forall_not_mem.trans
    ⟨fun h => le_bot_iff.1 (le_of_not_gt fun ε0 => h _ (mem_ball_self ε0)), fun ε0 _ h =>
      not_lt_of_le (le_of_eq ε0) (pos_of_mem_ball h)⟩
Characterization of Empty Extended Metric Ball: $B(x, \varepsilon) = \emptyset \leftrightarrow \varepsilon = 0$
Informal description
For any point $x$ in a pseudo extended metric space and any radius $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the extended metric ball $B(x, \varepsilon)$ is empty if and only if $\varepsilon = 0$.
EMetric.ordConnected_setOf_closedBall_subset theorem
(x : α) (s : Set α) : OrdConnected {r | closedBall x r ⊆ s}
Full source 
theorem ordConnected_setOf_closedBall_subset (x : α) (s : Set α) :
    OrdConnected { r | closedBall x r ⊆ s } :=
  ⟨fun _ _ _ h₁ _ h₂ => (closedBall_subset_closedBall h₂.2).trans h₁⟩
Order Connectedness of Radii for Which Closed Balls Are Subsets
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$ and any subset $s \subseteq \alpha$, the set of extended nonnegative real numbers $\{r \in \mathbb{R}_{\geq 0} \cup \{\infty\} \mid \text{closedBall}(x, r) \subseteq s\}$ is order connected. That is, for any $r_1, r_2$ in this set with $r_1 \leq r_2$, the entire interval $[r_1, r_2]$ is contained in the set.
EMetric.ordConnected_setOf_ball_subset theorem
(x : α) (s : Set α) : OrdConnected {r | ball x r ⊆ s}
Full source 
theorem ordConnected_setOf_ball_subset (x : α) (s : Set α) : OrdConnected { r | ball x r ⊆ s } :=
  ⟨fun _ _ _ h₁ _ h₂ => (ball_subset_ball h₂.2).trans h₁⟩
Order Connectedness of Radii for Ball Inclusion in Extended Metric Spaces
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$ and any subset $s \subseteq \alpha$, the set of radii $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ for which the extended metric ball $B(x, r)$ is contained in $s$ is order connected. That is, for any two radii $r_1, r_2$ in this set, the closed interval $[r_1, r_2]$ is entirely contained in the set.
EMetric.edistLtTopSetoid definition
: Setoid α
Full source 
/-- Relation “two points are at a finite edistance” is an equivalence relation. -/
def edistLtTopSetoid : Setoid α where
  r x y := edist x y < ⊤
  iseqv :=
    ⟨fun x => by rw [edist_self]; exact ENNReal.coe_lt_top,
      fun h => by rwa [edist_comm], fun hxy hyz =>
        lt_of_le_of_lt (edist_triangle _ _ _) (ENNReal.add_lt_top.2 ⟨hxy, hyz⟩)⟩
Finite extended distance equivalence relation
Informal description
The relation "two points are at a finite extended distance" is an equivalence relation on a type $\alpha$ equipped with an extended distance function $\text{edist} : \alpha \times \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$. Specifically, for any $x, y, z \in \alpha$: 1. Reflexivity: $\text{edist}(x, x) < \infty$. 2. Symmetry: $\text{edist}(x, y) < \infty$ if and only if $\text{edist}(y, x) < \infty$. 3. Transitivity: If $\text{edist}(x, y) < \infty$ and $\text{edist}(y, z) < \infty$, then $\text{edist}(x, z) < \infty$.
EMetric.ball_zero theorem
: ball x 0 = ∅
Full source 
@[simp]
theorem ball_zero : ball x 0 = ∅ := by rw [EMetric.ball_eq_empty_iff]
Empty Extended Metric Ball at Radius Zero
Informal description
For any point $x$ in a pseudo extended metric space, the extended metric ball centered at $x$ with radius $0$ is empty, i.e., $B(x, 0) = \emptyset$.
EMetric.nhds_basis_eball theorem
: (𝓝 x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) (ball x)
Full source 
theorem nhds_basis_eball : (𝓝 x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) (ball x) :=
  nhds_basis_uniformity uniformity_basis_edist
Neighborhood Basis via Extended Metric Balls
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the extended metric balls $\text{ball}(x, \varepsilon)$ for all $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
EMetric.nhdsWithin_basis_eball theorem
: (𝓝[s] x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => ball x ε ∩ s
Full source 
theorem nhdsWithin_basis_eball : (𝓝[s] x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => ballball x ε ∩ s :=
  nhdsWithin_hasBasis nhds_basis_eball s
Basis for Relative Neighborhood Filter via Extended Metric Balls
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$ and any subset $s \subseteq \alpha$, the neighborhood filter $\mathcal{N}_s(x)$ (neighborhoods of $x$ within $s$) has a basis consisting of the sets $\text{ball}(x, \varepsilon) \cap s$ for all $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
EMetric.nhds_basis_closed_eball theorem
: (𝓝 x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) (closedBall x)
Full source 
theorem nhds_basis_closed_eball : (𝓝 x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) (closedBall x) :=
  nhds_basis_uniformity uniformity_basis_edist_le
Neighborhood Basis via Closed Extended Balls
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the closed extended metric balls $\text{closedBall}(x, \varepsilon)$ for all $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$.
EMetric.nhdsWithin_basis_closed_eball theorem
: (𝓝[s] x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => closedBall x ε ∩ s
Full source 
theorem nhdsWithin_basis_closed_eball :
    (𝓝[s] x).HasBasis (fun ε : ℝ≥0∞ => 0 < ε) fun ε => closedBallclosedBall x ε ∩ s :=
  nhdsWithin_hasBasis nhds_basis_closed_eball s
Basis for Relative Neighborhood Filter via Closed Extended Balls
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$ and any subset $s \subseteq \alpha$, the neighborhood filter $\mathcal{N}_s(x)$ (neighborhoods of $x$ within $s$) has a basis consisting of the sets $\text{closedBall}(x, \varepsilon) \cap s$ for all $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, where $\text{closedBall}(x, \varepsilon) = \{ y \mid \text{edist}(y, x) \leq \varepsilon \}$.
EMetric.nhds_eq theorem
: 𝓝 x = ⨅ ε > 0, 𝓟 (ball x ε)
Full source 
theorem nhds_eq : 𝓝 x = ⨅ ε > 0, 𝓟 (ball x ε) :=
  nhds_basis_eball.eq_biInf
Neighborhood Filter Characterization via Extended Metric Balls
Informal description
In a pseudo extended metric space, the neighborhood filter $\mathcal{N}(x)$ of a point $x$ is equal to the infimum of the principal filters of all extended metric balls centered at $x$ with positive radius $\varepsilon$, i.e., \[ \mathcal{N}(x) = \bigsqcap_{\varepsilon > 0} \mathcal{P}(\text{ball}(x, \varepsilon)), \] where $\text{ball}(x, \varepsilon) = \{ y \mid \text{edist}(y, x) < \varepsilon \}$.
EMetric.mem_nhds_iff theorem
: s ∈ 𝓝 x ↔ ∃ ε > 0, ball x ε ⊆ s
Full source 
theorem mem_nhds_iff : s ∈ 𝓝 xs ∈ 𝓝 x ↔ ∃ ε > 0, ball x ε ⊆ s :=
  nhds_basis_eball.mem_iff
Neighborhood Characterization via Extended Metric Balls
Informal description
A subset $s$ of a pseudo extended metric space $\alpha$ is a neighborhood of a point $x \in \alpha$ if and only if there exists a positive radius $\varepsilon > 0$ such that the extended metric ball $\text{ball}(x, \varepsilon) = \{ y \mid \text{edist}(y, x) < \varepsilon \}$ is entirely contained in $s$.
EMetric.mem_nhdsWithin_iff theorem
: s ∈ 𝓝[t] x ↔ ∃ ε > 0, ball x ε ∩ t ⊆ s
Full source 
theorem mem_nhdsWithin_iff : s ∈ 𝓝[t] xs ∈ 𝓝[t] x ↔ ∃ ε > 0, ball x ε ∩ t ⊆ s :=
  nhdsWithin_basis_eball.mem_iff
Characterization of Relative Neighborhoods via Extended Metric Balls
Informal description
A subset $s$ of a pseudo extended metric space $\alpha$ is in the neighborhood filter within a subset $t$ at a point $x \in \alpha$ if and only if there exists a positive radius $\varepsilon > 0$ such that the intersection of the extended metric ball $\text{ball}(x, \varepsilon) = \{ y \mid \text{edist}(y, x) < \varepsilon \}$ with $t$ is contained in $s$.
EMetric.tendsto_nhdsWithin_nhdsWithin theorem
{t : Set β} {a b} : Tendsto f (𝓝[s] a) (𝓝[t] b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x⦄, x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε
Full source 
theorem tendsto_nhdsWithin_nhdsWithin {t : Set β} {a b} :
    TendstoTendsto f (𝓝[s] a) (𝓝[t] b) ↔
      ∀ ε > 0, ∃ δ > 0, ∀ ⦃x⦄, x ∈ s → edist x a < δ → f x ∈ t ∧ edist (f x) b < ε :=
  (nhdsWithin_basis_eball.tendsto_iff nhdsWithin_basis_eball).trans <|
    forall₂_congr fun ε _ => exists_congr fun δ => and_congr_right fun _ =>
      forall_congr' fun x => by simp; tauto
$\varepsilon$-$\delta$ Characterization of Relative Limits in Pseudo Extended Metric Spaces
Informal description
Let $f$ be a function between pseudo extended metric spaces $\alpha$ and $\beta$, with subsets $s \subseteq \alpha$ and $t \subseteq \beta$. Then $f$ tends to $b$ within $t$ as $x$ approaches $a$ within $s$ (i.e., $\lim_{\substack{x \to a \\ x \in s}} f(x) = b$ with $f(x) \in t$) if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists $\delta > 0$ such that for all $x \in s$ with $\text{edist}(x, a) < \delta$, we have $f(x) \in t$ and $\text{edist}(f(x), b) < \varepsilon$.
EMetric.tendsto_nhdsWithin_nhds theorem
{a b} : Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε
Full source 
theorem tendsto_nhdsWithin_nhds {a b} :
    TendstoTendsto f (𝓝[s] a) (𝓝 b) ↔
      ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε := by
  rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]
  simp only [mem_univ, true_and]
$\varepsilon$-$\delta$ Characterization of Relative Limits in Pseudo Extended Metric Spaces
Informal description
Let $f$ be a function between pseudo extended metric spaces $\alpha$ and $\beta$, with a subset $s \subseteq \alpha$. Then $f$ tends to $b$ at $a$ (i.e., $\lim_{x \to a} f(x) = b$) when $x$ is restricted to $s$ if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists $\delta > 0$ such that for all $x \in s$ with $\text{edist}(x, a) < \delta$, we have $\text{edist}(f(x), b) < \varepsilon$.
EMetric.tendsto_nhds_nhds theorem
{a b} : Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x⦄, edist x a < δ → edist (f x) b < ε
Full source 
theorem tendsto_nhds_nhds {a b} :
    TendstoTendsto f (𝓝 a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x⦄, edist x a < δ → edist (f x) b < ε :=
  nhds_basis_eball.tendsto_iff nhds_basis_eball
$\varepsilon$-$\delta$ Characterization of Limit in Pseudo Extended Metric Spaces
Informal description
Let $f$ be a function between pseudo extended metric spaces. Then $f$ tends to $b$ at $a$ (i.e., $\lim_{x \to a} f(x) = b$) if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists $\delta > 0$ such that for all $x$ with $\text{edist}(x, a) < \delta$, we have $\text{edist}(f(x), b) < \varepsilon$.
EMetric.isOpen_iff theorem
: IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s
Full source 
theorem isOpen_iff : IsOpenIsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s := by
  simp [isOpen_iff_nhds, mem_nhds_iff]
Characterization of Open Sets in Pseudo Extended Metric Spaces
Informal description
A subset $s$ of a pseudo extended metric space is open if and only if for every point $x \in s$, there exists a positive extended real number $\varepsilon > 0$ such that the extended metric ball $B(x, \varepsilon)$ centered at $x$ with radius $\varepsilon$ is entirely contained in $s$.
EMetric.isOpen_ball theorem
: IsOpen (ball x ε)
Full source 
@[simp] theorem isOpen_ball : IsOpen (ball x ε) :=
  isOpen_iff.2 fun _ => exists_ball_subset_ball
Openness of Extended Metric Balls
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$ and any radius $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the extended metric ball $B(x, \varepsilon) = \{y \in \alpha \mid \text{edist}(y, x) < \varepsilon\}$ is an open set.
EMetric.isClosed_ball_top theorem
: IsClosed (ball x ⊤)
Full source 
theorem isClosed_ball_top : IsClosed (ball x ⊤) :=
  isOpen_compl_iff.1 <| isOpen_iff.2 fun _y hy =>
    ⟨⊤, ENNReal.coe_lt_top, fun _z hzy hzx =>
      hy (edistLtTopSetoid.trans (edistLtTopSetoid.symm hzy) hzx)⟩
Closedness of Extended Metric Ball with Infinite Radius
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$, the extended metric ball $\text{ball}(x, \infty)$ is a closed set. Here, $\text{ball}(x, \infty)$ denotes the set of all points $y \in \alpha$ such that the extended distance $\text{edist}(y, x) < \infty$.
EMetric.ball_mem_nhds theorem
(x : α) {ε : ℝ≥0∞} (ε0 : 0 < ε) : ball x ε ∈ 𝓝 x
Full source 
theorem ball_mem_nhds (x : α) {ε : ℝ≥0∞} (ε0 : 0 < ε) : ballball x ε ∈ 𝓝 x :=
  isOpen_ball.mem_nhds (mem_ball_self ε0)
Extended Metric Balls are Neighborhoods of Their Centers
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$ and any radius $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $0 < \varepsilon$, the extended metric ball $\text{ball}(x, \varepsilon) = \{y \in \alpha \mid \text{edist}(y, x) < \varepsilon\}$ is a neighborhood of $x$.
EMetric.closedBall_mem_nhds theorem
(x : α) {ε : ℝ≥0∞} (ε0 : 0 < ε) : closedBall x ε ∈ 𝓝 x
Full source 
theorem closedBall_mem_nhds (x : α) {ε : ℝ≥0∞} (ε0 : 0 < ε) : closedBallclosedBall x ε ∈ 𝓝 x :=
  mem_of_superset (ball_mem_nhds x ε0) ball_subset_closedBall
Closed Balls are Neighborhoods of Their Centers in Extended Metric Spaces
Informal description
For any point $x$ in a pseudo extended metric space $\alpha$ and any radius $\varepsilon \in \mathbb{R}_{\geq 0} \cup \{\infty\}$ with $0 < \varepsilon$, the closed ball $\text{closedBall}(x, \varepsilon) = \{y \in \alpha \mid \text{edist}(y, x) \leq \varepsilon\}$ is a neighborhood of $x$.
EMetric.ball_prod_same theorem
[PseudoEMetricSpace β] (x : α) (y : β) (r : ℝ≥0∞) : ball x r ×ˢ ball y r = ball (x, y) r
Full source 
theorem ball_prod_same [PseudoEMetricSpace β] (x : α) (y : β) (r : ℝ≥0∞) :
    ball x r ×ˢ ball y r = ball (x, y) r :=
  ext fun z => by simp [Prod.edist_eq]
Product of Extended Metric Balls Equals Extended Metric Ball in Product Space
Informal description
Let $\alpha$ and $\beta$ be pseudo extended metric spaces. For any point $(x, y) \in \alpha \times \beta$ and any radius $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the Cartesian product of the extended metric balls $\text{ball}(x, r) \subseteq \alpha$ and $\text{ball}(y, r) \subseteq \beta$ is equal to the extended metric ball $\text{ball}((x, y), r) \subseteq \alpha \times \beta$ with respect to the maximum extended distance on the product space.
EMetric.closedBall_prod_same theorem
[PseudoEMetricSpace β] (x : α) (y : β) (r : ℝ≥0∞) : closedBall x r ×ˢ closedBall y r = closedBall (x, y) r
Full source 
theorem closedBall_prod_same [PseudoEMetricSpace β] (x : α) (y : β) (r : ℝ≥0∞) :
    closedBall x r ×ˢ closedBall y r = closedBall (x, y) r :=
  ext fun z => by simp [Prod.edist_eq]
Product of Closed Balls Equals Closed Ball in Product Space
Informal description
Let $\alpha$ and $\beta$ be pseudo extended metric spaces. For any points $x \in \alpha$, $y \in \beta$, and any extended nonnegative real number $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the Cartesian product of the closed balls $\text{closedBall}(x, r) \times \text{closedBall}(y, r)$ is equal to the closed ball $\text{closedBall}((x, y), r)$ in the product space $\alpha \times \beta$ equipped with the maximum extended distance.
EMetric.mem_closure_iff theorem
: x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε
Full source 
/-- ε-characterization of the closure in pseudoemetric spaces -/
theorem mem_closure_iff : x ∈ closure sx ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε :=
  (mem_closure_iff_nhds_basis nhds_basis_eball).trans <| by simp only [mem_ball, edist_comm x]
$\varepsilon$-Characterization of Closure in Pseudo Extended Metric Spaces
Informal description
Let $X$ be a pseudo extended metric space, $s \subseteq X$ a subset, and $x \in X$. Then $x$ belongs to the closure of $s$ if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists a point $y \in s$ such that the extended distance $\text{edist}(x, y) < \varepsilon$.
EMetric.tendsto_nhds theorem
{f : Filter β} {u : β → α} {a : α} : Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, edist (u x) a < ε
Full source 
theorem tendsto_nhds {f : Filter β} {u : β → α} {a : α} :
    TendstoTendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, edist (u x) a < ε :=
  nhds_basis_eball.tendsto_right_iff
Characterization of Convergence in Pseudo Extended Metric Spaces via Extended Distance
Informal description
Let $\alpha$ be a pseudo extended metric space, $\beta$ a type, $f$ a filter on $\beta$, and $u : \beta \to \alpha$ a function. Then $u$ tends to a point $a \in \alpha$ along the filter $f$ if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, the set $\{x \in \beta \mid \text{edist}(u(x), a) < \varepsilon\}$ is eventually in $f$.
EMetric.tendsto_atTop theorem
[Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε
Full source 
theorem tendsto_atTop [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} :
    TendstoTendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, edist (u n) a < ε :=
  (atTop_basis.tendsto_iff nhds_basis_eball).trans <| by
    simp only [exists_prop, true_and, mem_Ici, mem_ball]
Convergence in Pseudo Extended Metric Spaces via Extended Distance
Informal description
Let $\alpha$ be a pseudo extended metric space and $\beta$ be a nonempty directed set (join-semilattice). A function $u : \beta \to \alpha$ converges to a point $a \in \alpha$ with respect to the neighborhood filter $\mathcal{N}(a)$ if and only if for every $\varepsilon > 0$ in $\mathbb{R}_{\geq 0} \cup \{\infty\}$, there exists an index $N \in \beta$ such that for all $n \geq N$, the extended distance satisfies $\text{edist}(u(n), a) < \varepsilon$.
EMetric.subset_countable_closure_of_almost_dense_set theorem
(s : Set α) (hs : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε) : ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t
Full source 
/-- 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 subset_countable_closure_of_almost_dense_set (s : Set α)
    (hs : ∀ ε > 0, ∃ t : Set α, t.Countable ∧ s ⊆ ⋃ x ∈ t, closedBall x ε) :
    ∃ t, t ⊆ s ∧ t.Countable ∧ s ⊆ closure t := by
  rcases s.eq_empty_or_nonempty with (rfl | ⟨x₀, hx₀⟩)
  · exact ⟨∅, empty_subset _, countable_empty, empty_subset _⟩
  choose! T hTc hsT using fun n : ℕ => hs n⁻¹ (by simp)
  have : ∀ r x, ∃ y ∈ s, closedBall x r ∩ s ⊆ closedBall y (r * 2) := fun r x => by
    rcases (closedBallclosedBall x r ∩ s).eq_empty_or_nonempty with (he | ⟨y, hxy, hys⟩)
    · refine ⟨x₀, hx₀, ?_⟩
      rw [he]
      exact empty_subset _
    · refine ⟨y, hys, fun z hz => ?_⟩
      calc
        edist z y ≤ edist z x + edist y x := edist_triangle_right _ _ _
        _ ≤ r + r := add_le_add hz.1 hxy
        _ = r * 2 := (mul_two r).symm
  choose f hfs hf using this
  refine
    ⟨⋃ n : ℕ, f n⁻¹ '' T n, iUnion_subset fun n => image_subset_iff.2 fun z _ => hfs _ _,
      countable_iUnion fun n => (hTc n).image _, ?_⟩
  refine fun x hx => mem_closure_iff.2 fun ε ε0 => ?_
  rcases ENNReal.exists_inv_nat_lt (ENNReal.half_pos ε0.lt.ne').ne' with ⟨n, hn⟩
  rcases mem_iUnion₂.1 (hsT n hx) with ⟨y, hyn, hyx⟩
  refine ⟨f n⁻¹ y, mem_iUnion.2 ⟨n, mem_image_of_mem _ hyn⟩, ?_⟩
  calc
    edist x (f n⁻¹ y) ≤ (n : ℝ≥0∞)⁻¹ * 2 := hf _ _ ⟨hyx, hx⟩
    _ < ε := ENNReal.mul_lt_of_lt_div hn
Existence of Countable Dense Subset from $\varepsilon$-Dense Condition in Pseudo Extended Metric Spaces
Informal description
Let $s$ be a subset of a pseudo extended metric space $\alpha$. If for every $\varepsilon > 0$ there exists a countable subset $t \subseteq \alpha$ such that $s$ is covered by the union of closed balls of radius $\varepsilon$ centered at points of $t$, then there exists a countable subset $t' \subseteq s$ whose closure contains $s$.
EMetricSpace structure
(α : Type u) : Type u extends PseudoEMetricSpace α
Full source 
/-- An extended metric space is a type endowed with a `ℝ≥0∞`-valued distance `edist` satisfying
`edist x y = 0 ↔ x = y`, commutativity `edist x y = edist y x`, and the triangle inequality
`edist x z ≤ edist x y + edist y z`.

See pseudo extended metric spaces (`PseudoEMetricSpace`) for the similar class with the
`edist x y = 0 ↔ x = y` assumption weakened to `edist x x = 0`.

Any extended metric space is a T1 topological space and a uniform space (see `TopologicalSpace`,
`T1Space`, `UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This eg ensures that we do not get a diamond when doing
`[EMetricSpace α] [EMetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance]. -/
class EMetricSpace (α : Type u) : Type u extends PseudoEMetricSpace α where
  eq_of_edist_eq_zero : ∀ {x y : α}, edist x y = 0 → x = y
Extended Metric Space
Informal description
An extended metric space is a type $\alpha$ equipped with an extended distance function $\text{edist} : \alpha \times \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$ satisfying the following properties: 1. Non-degeneracy: $\text{edist}(x, y) = 0$ if and only if $x = y$. 2. Symmetry: $\text{edist}(x, y) = \text{edist}(y, x)$ for all $x, y \in \alpha$. 3. Triangle inequality: $\text{edist}(x, z) \leq \text{edist}(x, y) + \text{edist}(y, z)$ for all $x, y, z \in \alpha$. Any extended metric space naturally induces a T1 topological space structure and a uniform space structure, where the topology and uniformity are derived from the extended distance function. The uniformity and topology are included as part of the structure to avoid definitional inconsistencies in product spaces.
EMetricSpace.ext theorem
{α : Type*} {m m' : EMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m'
Full source 
@[ext]
protected theorem EMetricSpace.ext
    {α : Type*} {m m' : EMetricSpace α} (h : m.toEDist = m'.toEDist) : m = m' := by
  cases m
  cases m'
  congr
  ext1
  assumption
Uniqueness of Extended Metric Space Structure via Extended Distance
Informal description
Let $\alpha$ be a type, and let $m$ and $m'$ be two extended metric space structures on $\alpha$. If the extended distance functions of $m$ and $m'$ coincide, i.e., $m.\text{edist} = m'.\text{edist}$, then $m = m'$.
edist_eq_zero theorem
{x y : γ} : edist x y = 0 ↔ x = y
Full source 
/-- Characterize the equality of points by the vanishing of their extended distance -/
@[simp]
theorem edist_eq_zero {x y : γ} : edistedist x y = 0 ↔ x = y :=
  ⟨eq_of_edist_eq_zero, fun h => h ▸ edist_self _⟩
Vanishing Extended Distance Characterizes Equality
Informal description
For any two points $x$ and $y$ in an extended metric space $\gamma$, the extended distance $\text{edist}(x, y)$ is zero if and only if $x = y$.
zero_eq_edist theorem
{x y : γ} : 0 = edist x y ↔ x = y
Full source 
@[simp]
theorem zero_eq_edist {x y : γ} : 0 = edist x y ↔ x = y := eq_comm.trans edist_eq_zero
Zero Equals Extended Distance Characterizes Equality
Informal description
For any two points $x$ and $y$ in an extended metric space $\gamma$, the equality $0 = \text{edist}(x, y)$ holds if and only if $x = y$.
edist_le_zero theorem
{x y : γ} : edist x y ≤ 0 ↔ x = y
Full source 
theorem edist_le_zero {x y : γ} : edistedist x y ≤ 0 ↔ x = y :=
  nonpos_iff_eq_zero.trans edist_eq_zero
Nonpositive Extended Distance Characterizes Equality
Informal description
For any two points $x$ and $y$ in an extended metric space $\gamma$, the extended distance $\text{edist}(x, y)$ is less than or equal to zero if and only if $x = y$.
edist_pos theorem
{x y : γ} : 0 < edist x y ↔ x ≠ y
Full source 
@[simp]
theorem edist_pos {x y : γ} : 0 < edist x y ↔ x ≠ y := by simp [← not_le]
Positivity of Extended Distance Characterizes Inequality
Informal description
For any two points $x$ and $y$ in an extended metric space $\gamma$, the extended distance $\text{edist}(x, y)$ is strictly positive if and only if $x \neq y$.
EMetric.closedBall_zero theorem
(x : γ) : closedBall x 0 = { x }
Full source 
@[simp] lemma EMetric.closedBall_zero (x : γ) : closedBall x 0 = {x} := by ext; simp
Zero-Radius Closed Ball is Singleton Set
Informal description
For any point $x$ in an extended metric space $\gamma$, the closed ball centered at $x$ with radius $0$ is equal to the singleton set $\{x\}$.
EMetricSpace.replaceUniformity abbrev
{γ} [U : UniformSpace γ] (m : EMetricSpace γ) (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : EMetricSpace γ
Full source 
/-- 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.
See note [reducible non-instances].
-/
abbrev EMetricSpace.replaceUniformity {γ} [U : UniformSpace γ] (m : EMetricSpace γ)
    (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : EMetricSpace γ where
  edist := @edist _ m.toEDist
  edist_self := edist_self
  eq_of_edist_eq_zero := @eq_of_edist_eq_zero _ _
  edist_comm := edist_comm
  edist_triangle := edist_triangle
  toUniformSpace := U
  uniformity_edist := H.trans (@PseudoEMetricSpace.uniformity_edist γ _)
Construction of Extended Metric Space from Uniformity Condition
Informal description
Given a uniform space $\gamma$ with uniformity $\mathfrak{U}[U]$, and an extended metric space structure $m$ on $\gamma$ such that the uniformity $\mathfrak{U}[U]$ coincides with the uniformity induced by the extended metric, then $m$ can be used to construct a new extended metric space structure on $\gamma$ with the same uniformity.
EMetricSpace.induced abbrev
{γ β} (f : γ → β) (hf : Function.Injective f) (m : EMetricSpace β) : EMetricSpace γ
Full source 
/-- The extended metric induced by an injective function taking values in an emetric space.
See Note [reducible non-instances]. -/
abbrev EMetricSpace.induced {γ β} (f : γ → β) (hf : Function.Injective f) (m : EMetricSpace β) :
    EMetricSpace γ :=
  { PseudoEMetricSpace.induced f m.toPseudoEMetricSpace with
    eq_of_edist_eq_zero := fun h => hf (edist_eq_zero.1 h) }
Induced Extended Metric Space via Injective Function
Informal description
Given an injective function $f \colon \gamma \to \beta$ and an extended metric space structure on $\beta$, the induced extended metric space structure on $\gamma$ is defined by setting the extended distance between any two points $x, y \in \gamma$ to be $\text{edist}(f(x), f(y))$.
instEMetricSpaceSubtype instance
{α : Type*} {p : α → Prop} [EMetricSpace α] : EMetricSpace (Subtype p)
Full source 
/-- EMetric space instance on subsets of emetric spaces -/
instance {α : Type*} {p : α → Prop} [EMetricSpace α] : EMetricSpace (Subtype p) :=
  EMetricSpace.induced Subtype.val Subtype.coe_injective ‹_›
Extended Metric Space Structure on Subtypes
Informal description
For any extended metric space $\alpha$ and a predicate $p$ on $\alpha$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits an extended metric space structure from $\alpha$, where the extended distance between two points is defined as their distance in $\alpha$.
instEMetricSpaceMulOpposite instance
{α : Type*} [EMetricSpace α] : EMetricSpace αᵐᵒᵖ
Full source 
/-- EMetric space instance on the multiplicative opposite of an emetric space. -/
@[to_additive "EMetric space instance on the additive opposite of an emetric space."]
instance {α : Type*} [EMetricSpace α] : EMetricSpace αᵐᵒᵖ :=
  EMetricSpace.induced MulOpposite.unop MulOpposite.unop_injective ‹_›
Extended Metric Space Structure on Multiplicative Opposite
Informal description
The multiplicative opposite $\alpha^\text{op}$ of an extended metric space $\alpha$ inherits an extended metric space structure, where the extended distance between any two elements $x, y \in \alpha^\text{op}$ is defined as $\text{edist}(\text{unop}(x), \text{unop}(y))$, with $\text{unop} : \alpha^\text{op} \to \alpha$ being the canonical projection.
instEMetricSpaceULift instance
{α : Type*} [EMetricSpace α] : EMetricSpace (ULift α)
Full source 
instance {α : Type*} [EMetricSpace α] : EMetricSpace (ULift α) :=
  EMetricSpace.induced ULift.down ULift.down_injective ‹_›
Extended Metric Space Structure on Lifted Types
Informal description
For any extended metric space $\alpha$, the lifted type $\text{ULift}\,\alpha$ is also an extended metric space, where the extended distance function is inherited from $\alpha$.
uniformity_edist theorem
: 𝓤 γ = ⨅ ε > 0, 𝓟 {p : γ × γ | edist p.1 p.2 < ε}
Full source 
/-- Reformulation of the uniform structure in terms of the extended distance -/
theorem uniformity_edist : 𝓤 γ = ⨅ ε > 0, 𝓟 { p : γ × γ | edist p.1 p.2 < ε } :=
  PseudoEMetricSpace.uniformity_edist
Uniformity Filter Characterization via Extended Distance
Informal description
For an extended metric space $\gamma$, the uniformity filter $\mathfrak{U}(\gamma)$ is equal to the infimum over all positive $\varepsilon$ of the principal filter generated by the set $\{(x,y) \in \gamma \times \gamma \mid \text{edist}(x,y) < \varepsilon\}$.
instEDistAdditive instance
: EDist (Additive X)
Full source 
instance : EDist (Additive X) := ‹EDist X›
Extended Distance Structure on Additive Types
Informal description
For any type `X` equipped with an extended distance structure, the additive version of `X` (denoted `Additive X`) inherits the same extended distance structure. Specifically, the extended distance between two elements `a` and `b` in `Additive X` is equal to the extended distance between their corresponding elements in `X`.
instEDistMultiplicative instance
: EDist (Multiplicative X)
Full source 
instance : EDist (Multiplicative X) := ‹EDist X›
Extended Distance Structure on Multiplicative Types
Informal description
For any type `X` with an extended distance structure, the multiplicative version of `X` (denoted `Multiplicative X`) inherits the same extended distance structure.
edist_ofMul theorem
(a b : X) : edist (ofMul a) (ofMul b) = edist a b
Full source 
@[simp]
theorem edist_ofMul (a b : X) : edist (ofMul a) (ofMul b) = edist a b :=
  rfl
Multiplicative Embedding Preserves Extended Distance
Informal description
For any elements $a$ and $b$ of a type $X$ equipped with an extended distance function $\mathrm{edist}$, the extended distance between their images under the multiplicative embedding $\mathrm{ofMul}$ is equal to the extended distance between $a$ and $b$, i.e., \[ \mathrm{edist}(\mathrm{ofMul}\, a, \mathrm{ofMul}\, b) = \mathrm{edist}(a, b). \]
edist_ofAdd theorem
(a b : X) : edist (ofAdd a) (ofAdd b) = edist a b
Full source 
@[simp]
theorem edist_ofAdd (a b : X) : edist (ofAdd a) (ofAdd b) = edist a b :=
  rfl
Additive Embedding Preserves Extended Distance
Informal description
For any elements $a$ and $b$ of a type $X$ equipped with an extended distance function $\mathrm{edist}$, the extended distance between their images under the additive embedding $\mathrm{ofAdd}$ is equal to the extended distance between $a$ and $b$, i.e., \[ \mathrm{edist}(\mathrm{ofAdd}\, a, \mathrm{ofAdd}\, b) = \mathrm{edist}(a, b). \]
edist_toMul theorem
(a b : Additive X) : edist a.toMul b.toMul = edist a b
Full source 
@[simp]
theorem edist_toMul (a b : Additive X) : edist a.toMul b.toMul = edist a b :=
  rfl
Preservation of Extended Distance under Additive-to-Multiplicative Conversion
Informal description
For any elements $a$ and $b$ of the additive type `Additive X` equipped with an extended distance function $\mathrm{edist}$, the extended distance between their images under the conversion to the multiplicative type `X` is equal to the extended distance between $a$ and $b$, i.e., \[ \mathrm{edist}(a.\mathrm{toMul}, b.\mathrm{toMul}) = \mathrm{edist}(a, b). \]
edist_toAdd theorem
(a b : Multiplicative X) : edist a.toAdd b.toAdd = edist a b
Full source 
@[simp]
theorem edist_toAdd (a b : Multiplicative X) : edist a.toAdd b.toAdd = edist a b :=
  rfl
Preservation of Extended Distance under Multiplicative-to-Additive Conversion
Informal description
For any elements $a$ and $b$ of the multiplicative type `Multiplicative X` equipped with an extended distance function $\mathrm{edist}$, the extended distance between their images under the conversion to the additive type `X` is equal to the extended distance between $a$ and $b$, i.e., \[ \mathrm{edist}(a.\mathrm{toAdd}, b.\mathrm{toAdd}) = \mathrm{edist}(a, b). \]
instPseudoEMetricSpaceAdditive instance
[PseudoEMetricSpace X] : PseudoEMetricSpace (Additive X)
Full source 
instance [PseudoEMetricSpace X] : PseudoEMetricSpace (Additive X) := ‹PseudoEMetricSpace X›
Pseudo Extended Metric Space Structure on Additive Type Synonyms
Informal description
For any pseudo extended metric space $X$, the additive type synonym $\text{Additive}\, X$ inherits a pseudo extended metric space structure where the extended distance function is preserved.
instPseudoEMetricSpaceMultiplicative instance
[PseudoEMetricSpace X] : PseudoEMetricSpace (Multiplicative X)
Full source 
instance [PseudoEMetricSpace X] : PseudoEMetricSpace (Multiplicative X) := ‹PseudoEMetricSpace X›
Pseudo Extended Metric Space Structure on Multiplicative Types
Informal description
For any type `X` with a pseudo extended metric space structure, the multiplicative version of `X` (denoted as `Multiplicative X`) inherits the same pseudo extended metric space structure, where the extended distance function is preserved under the multiplicative operation.
instEMetricSpaceAdditive instance
[EMetricSpace X] : EMetricSpace (Additive X)
Full source 
instance [EMetricSpace X] : EMetricSpace (Additive X) := ‹EMetricSpace X›
Extended Metric Space Structure on Additive Type Synonyms
Informal description
For any extended metric space $X$, the additive type synonym $\text{Additive}\, X$ inherits an extended metric space structure where the distance function remains unchanged.
instEMetricSpaceMultiplicative instance
[EMetricSpace X] : EMetricSpace (Multiplicative X)
Full source 
instance [EMetricSpace X] : EMetricSpace (Multiplicative X) := ‹EMetricSpace X›
Extended Metric Space Structure on Multiplicative Type Synonyms
Informal description
For any extended metric space $X$, the multiplicative type synonym $\text{Multiplicative}\, X$ inherits an extended metric space structure where the distance function is preserved.
instEDistOrderDual instance
: EDist Xᵒᵈ
Full source 
instance : EDist Xᵒᵈ := ‹EDist X›
Extended Distance on Order Duals
Informal description
The order dual $X^{\text{op}}$ of a type $X$ with an extended distance function inherits the same extended distance structure, where the distance between two elements in $X^{\text{op}}$ is equal to the distance between their corresponding elements in $X$.
edist_toDual theorem
(a b : X) : edist (toDual a) (toDual b) = edist a b
Full source 
@[simp]
theorem edist_toDual (a b : X) : edist (toDual a) (toDual b) = edist a b :=
  rfl
Preservation of Extended Distance under Order Dual Map
Informal description
For any two elements $a$ and $b$ in a type $X$ equipped with an extended distance function, the extended distance between their images under the order dual map $\text{toDual} : X \to X^{\text{op}}$ is equal to the extended distance between $a$ and $b$ in $X$, i.e., \[ \text{edist}(\text{toDual}(a), \text{toDual}(b)) = \text{edist}(a, b). \]
edist_ofDual theorem
(a b : Xᵒᵈ) : edist (ofDual a) (ofDual b) = edist a b
Full source 
@[simp]
theorem edist_ofDual (a b : Xᵒᵈ) : edist (ofDual a) (ofDual b) = edist a b :=
  rfl
Preservation of Extended Distance under Order Dual Inverse Map
Informal description
For any two elements $a$ and $b$ in the order dual $X^{\text{op}}$ of a type $X$ equipped with an extended distance function, the extended distance between their images under the map $\text{ofDual} : X^{\text{op}} \to X$ is equal to the extended distance between $a$ and $b$ in $X^{\text{op}}$, i.e., \[ \text{edist}(\text{ofDual}(a), \text{ofDual}(b)) = \text{edist}(a, b). \]
instPseudoEMetricSpaceOrderDual instance
[PseudoEMetricSpace X] : PseudoEMetricSpace Xᵒᵈ
Full source 
instance [PseudoEMetricSpace X] : PseudoEMetricSpace Xᵒᵈ := ‹PseudoEMetricSpace X›
Pseudo Extended Metric Space Structure on Order Duals
Informal description
For any pseudo extended metric space $X$, the order dual $X^{\text{op}}$ is also a pseudo extended metric space with the same extended distance function.
instEMetricSpaceOrderDual instance
[EMetricSpace X] : EMetricSpace Xᵒᵈ
Full source 
instance [EMetricSpace X] : EMetricSpace Xᵒᵈ := ‹EMetricSpace X›
Extended Metric Space Structure on Order Duals
Informal description
For any extended metric space $X$, the order dual $X^{\text{op}}$ is also an extended metric space with the same extended distance function.