doc-next-gen

Mathlib.Topology.MetricSpace.Pseudo.Constructions

Module docstring

{"# Products of pseudometric spaces and other constructions

This file constructs the supremum distance on binary products of pseudometric spaces and provides instances for type synonyms. "}

PseudoMetricSpace.induced abbrev
{α β} (f : α → β) (m : PseudoMetricSpace β) : PseudoMetricSpace α
Full source 
/-- Pseudometric space structure pulled back by a function. -/
abbrev PseudoMetricSpace.induced {α β} (f : α → β) (m : PseudoMetricSpace β) :
    PseudoMetricSpace α where
  dist x y := dist (f x) (f y)
  dist_self _ := dist_self _
  dist_comm _ _ := dist_comm _ _
  dist_triangle _ _ _ := dist_triangle _ _ _
  edist x y := edist (f x) (f y)
  edist_dist _ _ := edist_dist _ _
  toUniformSpace := UniformSpace.comap f m.toUniformSpace
  uniformity_dist := (uniformity_basis_dist.comap _).eq_biInf
  toBornology := Bornology.induced f
  cobounded_sets := Set.ext fun s => mem_comap_iff_compl.trans <| by
    simp only [← isBounded_def, isBounded_iff, forall_mem_image, mem_setOf]
Induced Pseudometric Space via Function Pullback
Informal description
Given a function $f \colon \alpha \to \beta$ and a pseudometric space structure on $\beta$, the induced pseudometric space structure on $\alpha$ is defined by the distance function $\text{dist}(x, y) = \text{dist}(f(x), f(y))$ for all $x, y \in \alpha$.
Topology.IsInducing.comapPseudoMetricSpace definition
{α β : Type*} [TopologicalSpace α] [m : PseudoMetricSpace β] {f : α → β} (hf : IsInducing f) : PseudoMetricSpace α
Full source 
/-- Pull back a pseudometric space structure by an inducing map. This is a version of
`PseudoMetricSpace.induced` useful in case if the domain already has a `TopologicalSpace`
structure. -/
def Topology.IsInducing.comapPseudoMetricSpace {α β : Type*} [TopologicalSpace α]
    [m : PseudoMetricSpace β] {f : α → β} (hf : IsInducing f) : PseudoMetricSpace α :=
  .replaceTopology (.induced f m) hf.eq_induced
Pseudometric space structure induced by a topologically inducing map
Informal description
Given topological spaces $\alpha$ and $\beta$, where $\beta$ is equipped with a pseudometric space structure, and a continuous map $f \colon \alpha \to \beta$ that is inducing (i.e., the topology on $\alpha$ is the coarsest topology making $f$ continuous), the pseudometric space structure on $\alpha$ is defined by pulling back the pseudometric from $\beta$ via $f$ and ensuring compatibility with the existing topology on $\alpha$. Specifically, the distance function on $\alpha$ is given by $\text{dist}(x, y) = \text{dist}(f(x), f(y))$ for all $x, y \in \alpha$, and the topology induced by this distance coincides with the original topology on $\alpha$.
IsUniformInducing.comapPseudoMetricSpace definition
{α β} [UniformSpace α] [m : PseudoMetricSpace β] (f : α → β) (h : IsUniformInducing f) : PseudoMetricSpace α
Full source 
/-- Pull back a pseudometric space structure by a uniform inducing map. This is a version of
`PseudoMetricSpace.induced` useful in case if the domain already has a `UniformSpace`
structure. -/
def IsUniformInducing.comapPseudoMetricSpace {α β} [UniformSpace α] [m : PseudoMetricSpace β]
    (f : α → β) (h : IsUniformInducing f) : PseudoMetricSpace α :=
  .replaceUniformity (.induced f m) h.comap_uniformity.symm
Pseudometric space structure induced by a uniform inducing map
Informal description
Given a uniform space $\alpha$, a pseudometric space $\beta$, and a uniform inducing map $f \colon \alpha \to \beta$, the pseudometric space structure on $\alpha$ is defined by pulling back the pseudometric from $\beta$ via $f$ and ensuring compatibility with the existing uniform structure on $\alpha$. Specifically, the distance function on $\alpha$ is given by $\text{dist}(x, y) = \text{dist}(f(x), f(y))$ for all $x, y \in \alpha$, and the uniformity induced by this distance coincides with the original uniformity on $\alpha$.
Subtype.pseudoMetricSpace instance
{p : α → Prop} : PseudoMetricSpace (Subtype p)
Full source 
instance Subtype.pseudoMetricSpace {p : α → Prop} : PseudoMetricSpace (Subtype p) :=
  PseudoMetricSpace.induced Subtype.val ‹_›
Pseudometric Space Structure on Subtypes
Informal description
For any subset of a pseudometric space $\alpha$ defined by a predicate $p : \alpha \to \text{Prop}$, the subtype $\{x \in \alpha \mid p(x)\}$ inherits a pseudometric space structure from $\alpha$, where the distance between two elements $x$ and $y$ in the subtype is equal to the distance between them in $\alpha$.
Subtype.dist_eq theorem
{p : α → Prop} (x y : Subtype p) : dist x y = dist (x : α) y
Full source 
lemma Subtype.dist_eq {p : α → Prop} (x y : Subtype p) : dist x y = dist (x : α) y := rfl
Distance Equality in Subtype of Pseudometric Space
Informal description
For any subset $\{x \in \alpha \mid p(x)\}$ of a pseudometric space $\alpha$, the distance between two elements $x$ and $y$ in the subset is equal to the distance between them in the ambient space $\alpha$, i.e., $\text{dist}(x, y) = \text{dist}(x, y)$.
Subtype.nndist_eq theorem
{p : α → Prop} (x y : Subtype p) : nndist x y = nndist (x : α) y
Full source 
lemma Subtype.nndist_eq {p : α → Prop} (x y : Subtype p) : nndist x y = nndist (x : α) y := rfl
Non-negative Distance Equality in Subtype of Pseudometric Space
Informal description
For any subset of a pseudometric space $\alpha$ defined by a predicate $p : \alpha \to \text{Prop}$, the non-negative distance between two elements $x$ and $y$ in the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the non-negative distance between $x$ and $y$ when viewed as elements of $\alpha$.
MulOpposite.instPseudoMetricSpace instance
: PseudoMetricSpace αᵐᵒᵖ
Full source 
@[to_additive]
instance instPseudoMetricSpace : PseudoMetricSpace αᵐᵒᵖ :=
  PseudoMetricSpace.induced MulOpposite.unop ‹_›
Pseudometric Space Structure on Multiplicative Opposite
Informal description
The multiplicative opposite $\alpha^\text{op}$ of a pseudometric space $\alpha$ inherits a pseudometric space structure, where the distance between two elements $x$ and $y$ in $\alpha^\text{op}$ is equal to the distance between their corresponding elements in $\alpha$.
MulOpposite.dist_unop theorem
(x y : αᵐᵒᵖ) : dist (unop x) (unop y) = dist x y
Full source 
@[to_additive (attr := simp)]
lemma dist_unop (x y : αᵐᵒᵖ) : dist (unop x) (unop y) = dist x y := rfl
Distance Preservation under Projection from Multiplicative Opposite
Informal description
For any two elements $x, y$ in the multiplicative opposite $\alpha^\text{op}$ of a pseudometric space $\alpha$, the distance between their projections back to $\alpha$ is equal to the distance between $x$ and $y$ in $\alpha^\text{op}$. That is, $\text{dist}(\text{unop}(x), \text{unop}(y)) = \text{dist}(x, y)$.
MulOpposite.dist_op theorem
(x y : α) : dist (op x) (op y) = dist x y
Full source 
@[to_additive (attr := simp)]
lemma dist_op (x y : α) : dist (op x) (op y) = dist x y := rfl
Distance Preservation under Multiplicative Opposite Embedding
Informal description
For any two elements $x$ and $y$ in a pseudometric space $\alpha$, the distance between their images under the canonical embedding into the multiplicative opposite $\alpha^\text{op}$ is equal to the distance between $x$ and $y$ in $\alpha$. That is, $\text{dist}(\text{op}(x), \text{op}(y)) = \text{dist}(x, y)$.
MulOpposite.nndist_unop theorem
(x y : αᵐᵒᵖ) : nndist (unop x) (unop y) = nndist x y
Full source 
@[to_additive (attr := simp)]
lemma nndist_unop (x y : αᵐᵒᵖ) : nndist (unop x) (unop y) = nndist x y := rfl
Non-negative Distance Preservation under Projection from Multiplicative Opposite
Informal description
For any two elements $x$ and $y$ in the multiplicative opposite $\alpha^\text{op}$ of a pseudometric space $\alpha$, the non-negative distance between their projections $\text{unop}(x)$ and $\text{unop}(y)$ in $\alpha$ is equal to the non-negative distance between $x$ and $y$ in $\alpha^\text{op}$. That is, $\text{nndist}(\text{unop}(x), \text{unop}(y)) = \text{nndist}(x, y)$.
MulOpposite.nndist_op theorem
(x y : α) : nndist (op x) (op y) = nndist x y
Full source 
@[to_additive (attr := simp)]
lemma nndist_op (x y : α) : nndist (op x) (op y) = nndist x y := rfl
Non-Negative Distance Preservation under Multiplicative Opposite
Informal description
For any two elements $x$ and $y$ in a pseudometric space $\alpha$, the non-negative distance between their multiplicative opposites $\text{op}(x)$ and $\text{op}(y)$ in $\alpha^\text{op}$ is equal to the non-negative distance between $x$ and $y$ in $\alpha$. That is, $\text{nndist}(\text{op}(x), \text{op}(y)) = \text{nndist}(x, y)$.
instPseudoMetricSpaceNNReal instance
: PseudoMetricSpace ℝ≥0
Full source 
instance : PseudoMetricSpace ℝ≥0 := Subtype.pseudoMetricSpace
The Pseudometric Space Structure on Non-Negative Real Numbers
Informal description
The non-negative real numbers $\mathbb{R}_{\geq 0}$ are equipped with a canonical pseudometric space structure, where the distance function is given by $\text{dist}(x, y) = |x - y|$ for all $x, y \in \mathbb{R}_{\geq 0}$.
NNReal.dist_eq theorem
(a b : ℝ≥0) : dist a b = |(a : ℝ) - b|
Full source 
lemma NNReal.dist_eq (a b : ℝ≥0) : dist a b = |(a : ℝ) - b| := rfl
Distance Formula for Non-Negative Real Numbers: $\text{dist}(a, b) = |a - b|$
Informal description
For any two non-negative real numbers $a$ and $b$, the distance between them is equal to the absolute value of their difference when viewed as real numbers, i.e., $\text{dist}(a, b) = |a - b|$.
NNReal.nndist_eq theorem
(a b : ℝ≥0) : nndist a b = max (a - b) (b - a)
Full source 
lemma NNReal.nndist_eq (a b : ℝ≥0) : nndist a b = max (a - b) (b - a) :=
  eq_of_forall_ge_iff fun _ => by
    simp only [max_le_iff, tsub_le_iff_right (α := ℝ≥0)]
    simp only [← NNReal.coe_le_coe, coe_nndist, dist_eq, abs_sub_le_iff,
      tsub_le_iff_right, NNReal.coe_add]
Non-negative Distance Formula for Non-Negative Reals: $\text{nndist}(a, b) = \max(a - b, b - a)$
Informal description
For any two non-negative real numbers $a$ and $b$, the non-negative distance between them is equal to the maximum of $a - b$ and $b - a$, i.e., $\text{nndist}(a, b) = \max(a - b, b - a)$.
NNReal.nndist_zero_eq_val' theorem
(z : ℝ≥0) : nndist z 0 = z
Full source 
@[simp]
lemma NNReal.nndist_zero_eq_val' (z : ℝ≥0) : nndist z 0 = z := by
  rw [nndist_comm]
  exact NNReal.nndist_zero_eq_val z
Distance to Zero in Non-Negative Reals: $\text{nndist}(z, 0) = z$
Informal description
For any non-negative real number $z$, the non-negative distance from $z$ to $0$ is equal to $z$, i.e., $\text{nndist}(z, 0) = z$.
NNReal.le_add_nndist theorem
(a b : ℝ≥0) : a ≤ b + nndist a b
Full source 
lemma NNReal.le_add_nndist (a b : ℝ≥0) : a ≤ b + nndist a b := by
  suffices (a : ℝ) ≤ (b : ℝ) + dist a b by
    rwa [← NNReal.coe_le_coe, NNReal.coe_add, coe_nndist]
  rw [← sub_le_iff_le_add']
  exact le_of_abs_le (dist_eq a b).ge
Inequality Relating Non-Negative Real Numbers and Their Distance: $a \leq b + \text{nndist}(a, b)$
Informal description
For any two non-negative real numbers $a$ and $b$, the inequality $a \leq b + \text{nndist}(a, b)$ holds, where $\text{nndist}(a, b)$ is the non-negative distance between $a$ and $b$.
NNReal.ball_zero_eq_Ico' theorem
(c : ℝ≥0) : Metric.ball (0 : ℝ≥0) c.toReal = Set.Ico 0 c
Full source 
lemma NNReal.ball_zero_eq_Ico' (c : ℝ≥0) :
    Metric.ball (0 : ℝ≥0) c.toReal = Set.Ico 0 c := by ext x; simp
Open Ball at Zero in Non-Negative Reals Equals Interval $[0, c)$
Informal description
For any non-negative real number $c$, the open ball centered at $0$ with radius $c$ (as a real number) in the pseudometric space of non-negative real numbers is equal to the left-closed right-open interval $[0, c)$, i.e., $\text{ball}(0, c) = [0, c)$.
NNReal.ball_zero_eq_Ico theorem
(c : ℝ) : Metric.ball (0 : ℝ≥0) c = Set.Ico 0 c.toNNReal
Full source 
lemma NNReal.ball_zero_eq_Ico (c : ℝ) :
    Metric.ball (0 : ℝ≥0) c = Set.Ico 0 c.toNNReal := by
  by_cases c_pos : 0 < c
  · convert NNReal.ball_zero_eq_Ico' ⟨c, c_pos.le⟩
    simp [Real.toNNReal, c_pos.le]
  simp [not_lt.mp c_pos]
Open Ball at Zero in Non-Negative Reals Equals Interval $[0, c_{\geq 0})$
Informal description
For any real number $c$, the open ball centered at $0$ with radius $c$ in the pseudometric space of non-negative real numbers is equal to the left-closed right-open interval $[0, c_{\geq 0})$, where $c_{\geq 0}$ is the non-negative part of $c$. That is, $\text{ball}(0, c) = [0, c_{\geq 0})$.
NNReal.closedBall_zero_eq_Icc' theorem
(c : ℝ≥0) : Metric.closedBall (0 : ℝ≥0) c.toReal = Set.Icc 0 c
Full source 
lemma NNReal.closedBall_zero_eq_Icc' (c : ℝ≥0) :
    Metric.closedBall (0 : ℝ≥0) c.toReal = Set.Icc 0 c := by ext x; simp
Closed Ball at Zero in Non-Negative Reals Equals Closed Interval $[0, c]$
Informal description
For any non-negative real number $c$, the closed ball centered at $0$ with radius $c$ in the pseudometric space of non-negative real numbers is equal to the closed interval $[0, c]$. That is, $\overline{B}(0, c) = [0, c]$.
NNReal.closedBall_zero_eq_Icc theorem
{c : ℝ} (c_nn : 0 ≤ c) : Metric.closedBall (0 : ℝ≥0) c = Set.Icc 0 c.toNNReal
Full source 
lemma NNReal.closedBall_zero_eq_Icc {c : ℝ} (c_nn : 0 ≤ c) :
    Metric.closedBall (0 : ℝ≥0) c = Set.Icc 0 c.toNNReal := by
  convert NNReal.closedBall_zero_eq_Icc' ⟨c, c_nn⟩
  simp [Real.toNNReal, c_nn]
Closed Ball at Zero in Non-Negative Reals Equals Closed Interval $[0, c_{\text{NN}}]$
Informal description
For any real number $c \geq 0$, the closed ball centered at $0$ with radius $c$ in the pseudometric space of non-negative real numbers is equal to the closed interval $[0, c_{\text{NN}}]$, where $c_{\text{NN}}$ is the non-negative real number corresponding to $c$. That is, $\overline{B}(0, c) = [0, c_{\text{NN}}]$.
ULift.instPseudoMetricSpace instance
: PseudoMetricSpace (ULift β)
Full source 
instance : PseudoMetricSpace (ULift β) := PseudoMetricSpace.induced ULift.down ‹_›
Pseudometric Space Structure on Universe-Lifted Types
Informal description
For any pseudometric space $\beta$, the type `ULift β` (which represents $\beta$ lifted to a different universe) inherits a pseudometric space structure where the distance between two lifted elements is equal to the distance between their underlying elements in $\beta$.
ULift.dist_eq theorem
(x y : ULift β) : dist x y = dist x.down y.down
Full source 
lemma dist_eq (x y : ULift β) : dist x y = dist x.down y.down := rfl
Distance Preservation in Universe-Lifted Pseudometric Spaces
Informal description
For any two elements $x$ and $y$ in the universe-lifted type $\text{ULift} \beta$, the distance between them is equal to the distance between their underlying elements in $\beta$, i.e., $\text{dist}(x, y) = \text{dist}(x.\text{down}, y.\text{down})$.
ULift.nndist_eq theorem
(x y : ULift β) : nndist x y = nndist x.down y.down
Full source 
lemma nndist_eq (x y : ULift β) : nndist x y = nndist x.down y.down := rfl
Non-negative Distance Preservation under Universe Lifting
Informal description
For any two elements $x$ and $y$ in the universe-lifted type $\text{ULift}\,\beta$, the non-negative distance between them is equal to the non-negative distance between their underlying elements in $\beta$, i.e., $\text{nndist}(x, y) = \text{nndist}(x.\text{down}, y.\text{down})$.
ULift.dist_up_up theorem
(x y : β) : dist (ULift.up x) (ULift.up y) = dist x y
Full source 
@[simp] lemma dist_up_up (x y : β) : dist (ULift.up x) (ULift.up y) = dist x y := rfl
Distance Preservation under Universe Lifting: $\text{dist}(\text{up}(x), \text{up}(y)) = \text{dist}(x, y)$
Informal description
For any two elements $x$ and $y$ in a pseudometric space $\beta$, the distance between their lifts $\text{up}(x)$ and $\text{up}(y)$ in $\text{ULift}\,\beta$ is equal to the distance between $x$ and $y$ in $\beta$, i.e., $\text{dist}(\text{up}(x), \text{up}(y)) = \text{dist}(x, y)$.
ULift.nndist_up_up theorem
(x y : β) : nndist (ULift.up x) (ULift.up y) = nndist x y
Full source 
@[simp] lemma nndist_up_up (x y : β) : nndist (ULift.up x) (ULift.up y) = nndist x y := rfl
Non-negative Distance Preservation under Universe Lifting
Informal description
For any two elements $x$ and $y$ in a pseudometric space $\beta$, the non-negative distance between their lifts $\text{up}(x)$ and $\text{up}(y)$ in $\text{ULift}(\beta)$ is equal to the non-negative distance between $x$ and $y$ in $\beta$, i.e., $\text{nndist}(\text{up}(x), \text{up}(y)) = \text{nndist}(x, y)$.
Prod.pseudoMetricSpaceMax instance
: PseudoMetricSpace (α × β)
Full source 
instance Prod.pseudoMetricSpaceMax : PseudoMetricSpace (α × β) :=
  let i := PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun x y : α × β => distdist x.1 y.1 ⊔ dist x.2 y.2)
    (fun _ _ => (max_lt (edist_lt_top _ _) (edist_lt_top _ _)).ne) fun x y => by
      simp only [dist_edist, ← ENNReal.toReal_max (edist_ne_top _ _) (edist_ne_top _ _),
        Prod.edist_eq]
  i.replaceBornology fun s => by
    simp only [← isBounded_image_fst_and_snd, isBounded_iff_eventually, forall_mem_image, ←
      eventually_and, ← forall_and, ← max_le_iff]
    rfl
Product Pseudometric Space with Supremum Distance
Informal description
The product $\alpha \times \beta$ of two pseudometric spaces $\alpha$ and $\beta$ can be equipped with a pseudometric space structure where the distance between two points $(x_1, y_1)$ and $(x_2, y_2)$ is defined as the maximum of the distances $\text{dist}(x_1, x_2)$ and $\text{dist}(y_1, y_2)$.
Prod.dist_eq theorem
{x y : α × β} : dist x y = max (dist x.1 y.1) (dist x.2 y.2)
Full source 
lemma Prod.dist_eq {x y : α × β} : dist x y = max (dist x.1 y.1) (dist x.2 y.2) := rfl
Distance Formula for Product Pseudometric Space: $\text{dist}(x, y) = \max(\text{dist}(x_1, y_1), \text{dist}(x_2, y_2))$
Informal description
For any two points $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product pseudometric space $\alpha \times \beta$, the distance between $x$ and $y$ is equal to the maximum of the distances between their components, i.e., \[ \text{dist}(x, y) = \max(\text{dist}(x_1, y_1), \text{dist}(x_2, y_2)). \]
dist_prod_same_left theorem
{x : α} {y₁ y₂ : β} : dist (x, y₁) (x, y₂) = dist y₁ y₂
Full source 
@[simp]
lemma dist_prod_same_left {x : α} {y₁ y₂ : β} : dist (x, y₁) (x, y₂) = dist y₁ y₂ := by
  simp [Prod.dist_eq, dist_nonneg]
Distance in Product Space Along Fixed First Coordinate: $\text{dist}((x, y_1), (x, y_2)) = \text{dist}(y_1, y_2)$
Informal description
For any point $x$ in a pseudometric space $\alpha$ and any two points $y_1, y_2$ in a pseudometric space $\beta$, the distance between $(x, y_1)$ and $(x, y_2)$ in the product space $\alpha \times \beta$ is equal to the distance between $y_1$ and $y_2$ in $\beta$, i.e., $\text{dist}((x, y_1), (x, y_2)) = \text{dist}(y_1, y_2)$.
dist_prod_same_right theorem
{x₁ x₂ : α} {y : β} : dist (x₁, y) (x₂, y) = dist x₁ x₂
Full source 
@[simp]
lemma dist_prod_same_right {x₁ x₂ : α} {y : β} : dist (x₁, y) (x₂, y) = dist x₁ x₂ := by
  simp [Prod.dist_eq, dist_nonneg]
Distance Preservation in Product Space (Right Component Fixed)
Informal description
For any points $x_1, x_2$ in a pseudometric space $\alpha$ and any point $y$ in a pseudometric space $\beta$, the distance between $(x_1, y)$ and $(x_2, y)$ in the product space $\alpha \times \beta$ equals the distance between $x_1$ and $x_2$ in $\alpha$, i.e., $\text{dist}((x_1, y), (x_2, y)) = \text{dist}(x_1, x_2)$.
ball_prod_same theorem
(x : α) (y : β) (r : ℝ) : ball x r ×ˢ ball y r = ball (x, y) r
Full source 
lemma ball_prod_same (x : α) (y : β) (r : ℝ) : ball x r ×ˢ ball y r = ball (x, y) r :=
  ext fun z => by simp [Prod.dist_eq]
Product of Open Balls Equals Open Ball in Product Space
Informal description
For any point $(x, y)$ in the product pseudometric space $\alpha \times \beta$ and any positive real number $r$, the Cartesian product of the open balls $\text{ball}(x, r) \times \text{ball}(y, r)$ is equal to the open ball $\text{ball}((x, y), r)$ in the product space with the supremum distance.
closedBall_prod_same theorem
(x : α) (y : β) (r : ℝ) : closedBall x r ×ˢ closedBall y r = closedBall (x, y) r
Full source 
lemma closedBall_prod_same (x : α) (y : β) (r : ℝ) :
    closedBall x r ×ˢ closedBall y r = closedBall (x, y) r := ext fun z => by simp [Prod.dist_eq]
Product of Closed Balls Equals Closed Ball in Product Space with Supremum Distance
Informal description
For any point $x$ in a pseudometric space $\alpha$, any point $y$ in a pseudometric space $\beta$, and any non-negative real number $r$, the Cartesian product of the closed balls $\overline{B}(x, r) \times \overline{B}(y, r)$ is equal to the closed ball $\overline{B}((x, y), r)$ in the product space $\alpha \times \beta$ equipped with the supremum distance.
sphere_prod theorem
(x : α × β) (r : ℝ) : sphere x r = sphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r
Full source 
lemma sphere_prod (x : α × β) (r : ℝ) :
    sphere x r = spheresphere x.1 r ×ˢ closedBall x.2 r ∪ closedBall x.1 r ×ˢ sphere x.2 r := by
  obtain hr | rfl | hr := lt_trichotomy r 0
  · simp [hr]
  · cases x
    simp_rw [← closedBall_eq_sphere_of_nonpos le_rfl, union_self, closedBall_prod_same]
  · ext ⟨x', y'⟩
    simp_rw [Set.mem_union, Set.mem_prod, Metric.mem_closedBall, Metric.mem_sphere, Prod.dist_eq,
      max_eq_iff]
    refine or_congr (and_congr_right ?_) (and_comm.trans (and_congr_left ?_))
    all_goals rintro rfl; rfl
Decomposition of Sphere in Product Space with Supremum Distance
Informal description
For any point $x = (x_1, x_2)$ in the product pseudometric space $\alpha \times \beta$ and any real number $r$, the sphere centered at $x$ with radius $r$ is equal to the union of: 1. The Cartesian product of the sphere centered at $x_1$ with radius $r$ in $\alpha$ and the closed ball centered at $x_2$ with radius $r$ in $\beta$, and 2. The Cartesian product of the closed ball centered at $x_1$ with radius $r$ in $\alpha$ and the sphere centered at $x_2$ with radius $r$ in $\beta$. In symbols: $$\text{sphere}(x, r) = \text{sphere}(x_1, r) \times \overline{B}(x_2, r) \cup \overline{B}(x_1, r) \times \text{sphere}(x_2, r)$$
uniformContinuous_dist theorem
: UniformContinuous fun p : α × α => dist p.1 p.2
Full source 
lemma uniformContinuous_dist : UniformContinuous fun p : α × α => dist p.1 p.2 :=
  Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨ε / 2, half_pos ε0, fun {a b} h =>
      calc dist (dist a.1 a.2) (dist b.1 b.2) ≤ dist a.1 b.1 + dist a.2 b.2 :=
        dist_dist_dist_le _ _ _ _
      _ ≤ dist a b + dist a b := add_le_add (le_max_left _ _) (le_max_right _ _)
      _ < ε / 2 + ε / 2 := add_lt_add h h
      _ = ε := add_halves ε⟩
Uniform Continuity of the Distance Function in Pseudometric Spaces
Informal description
The distance function $\text{dist} \colon \alpha \times \alpha \to \mathbb{R}$ is uniformly continuous when $\alpha$ is a pseudometric space and $\alpha \times \alpha$ is equipped with the product uniform structure.
UniformContinuous.dist theorem
[UniformSpace β] {f g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun b => dist (f b) (g b)
Full source 
protected lemma UniformContinuous.dist [UniformSpace β] {f g : β → α} (hf : UniformContinuous f)
    (hg : UniformContinuous g) : UniformContinuous fun b => dist (f b) (g b) :=
  uniformContinuous_dist.comp (hf.prodMk hg)
Uniform continuity of the distance between uniformly continuous functions
Informal description
Let $\alpha$ be a pseudometric space and $\beta$ be a uniform space. For any two uniformly continuous functions $f, g \colon \beta \to \alpha$, the function $b \mapsto \text{dist}(f(b), g(b))$ from $\beta$ to $\mathbb{R}$ is uniformly continuous.
continuous_dist theorem
: Continuous fun p : α × α ↦ dist p.1 p.2
Full source 
@[continuity]
lemma continuous_dist : Continuous fun p : α × α ↦ dist p.1 p.2 := uniformContinuous_dist.continuous
Continuity of the Distance Function in Pseudometric Spaces
Informal description
The distance function $\text{dist} \colon \alpha \times \alpha \to \mathbb{R}$ is continuous when $\alpha$ is a pseudometric space and $\alpha \times \alpha$ is equipped with the product topology.
Continuous.dist theorem
[TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : Continuous fun b => dist (f b) (g b)
Full source 
@[continuity, fun_prop]
protected lemma Continuous.dist [TopologicalSpace β] {f g : β → α} (hf : Continuous f)
    (hg : Continuous g) : Continuous fun b => dist (f b) (g b) :=
  continuous_dist.comp₂ hf hg
Continuity of the Distance Between Continuous Functions
Informal description
Let $\alpha$ be a pseudometric space and $\beta$ be a topological space. For any two continuous functions $f, g \colon \beta \to \alpha$, the function $b \mapsto \text{dist}(f(b), g(b))$ from $\beta$ to $\mathbb{R}$ is continuous.
Filter.Tendsto.dist theorem
{f g : β → α} {x : Filter β} {a b : α} (hf : Tendsto f x (𝓝 a)) (hg : Tendsto g x (𝓝 b)) : Tendsto (fun x => dist (f x) (g x)) x (𝓝 (dist a b))
Full source 
protected lemma Filter.Tendsto.dist {f g : β → α} {x : Filter β} {a b : α}
    (hf : Tendsto f x (𝓝 a)) (hg : Tendsto g x (𝓝 b)) :
    Tendsto (fun x => dist (f x) (g x)) x (𝓝 (dist a b)) :=
  (continuous_dist.tendsto (a, b)).comp (hf.prodMk_nhds hg)
Limit of Distance Function under Convergent Functions
Informal description
Let $X$ be a topological space and $\alpha$ be a pseudometric space. For any functions $f, g \colon X \to \alpha$ and any filter $x$ on $X$, if $f$ tends to $a \in \alpha$ along $x$ and $g$ tends to $b \in \alpha$ along $x$, then the function $x \mapsto \text{dist}(f(x), g(x))$ tends to $\text{dist}(a, b)$ along $x$.
continuous_iff_continuous_dist theorem
[TopologicalSpace β] {f : β → α} : Continuous f ↔ Continuous fun x : β × β => dist (f x.1) (f x.2)
Full source 
lemma continuous_iff_continuous_dist [TopologicalSpace β] {f : β → α} :
    ContinuousContinuous f ↔ Continuous fun x : β × β => dist (f x.1) (f x.2) :=
  ⟨fun h => h.fst'.dist h.snd', fun h =>
    continuous_iff_continuousAt.2 fun _ => tendsto_iff_dist_tendsto_zero.2 <|
      (h.comp (.prodMk_left _)).tendsto' _ _ <| dist_self _⟩
Characterization of Continuity via Distance Function
Informal description
Let $\alpha$ be a pseudometric space and $\beta$ be a topological space. A function $f \colon \beta \to \alpha$ is continuous if and only if the function $(x, y) \mapsto \text{dist}(f(x), f(y))$ from $\beta \times \beta$ to $\mathbb{R}$ is continuous.
uniformContinuous_nndist theorem
: UniformContinuous fun p : α × α => nndist p.1 p.2
Full source 
lemma uniformContinuous_nndist : UniformContinuous fun p : α × α => nndist p.1 p.2 :=
  uniformContinuous_dist.subtype_mk _
Uniform Continuity of Non-Negative Distance Function in Pseudometric Spaces
Informal description
The non-negative distance function $\text{nndist} \colon \alpha \times \alpha \to \mathbb{R}_{\geq 0}$ is uniformly continuous when $\alpha$ is a pseudometric space and $\alpha \times \alpha$ is equipped with the product uniform structure.
UniformContinuous.nndist theorem
[UniformSpace β] {f g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) : UniformContinuous fun b => nndist (f b) (g b)
Full source 
protected lemma UniformContinuous.nndist [UniformSpace β] {f g : β → α} (hf : UniformContinuous f)
    (hg : UniformContinuous g) : UniformContinuous fun b => nndist (f b) (g b) :=
  uniformContinuous_nndist.comp (hf.prodMk hg)
Uniform Continuity of the Non-Negative Distance Between Uniformly Continuous Functions
Informal description
Let $\alpha$ be a pseudometric space and $\beta$ be a uniform space. For any two uniformly continuous functions $f, g \colon \beta \to \alpha$, the function $b \mapsto \text{nndist}(f(b), g(b))$ from $\beta$ to $\mathbb{R}_{\geq 0}$ is uniformly continuous, where $\text{nndist}$ denotes the non-negative distance function on $\alpha$.
continuous_nndist theorem
: Continuous fun p : α × α => nndist p.1 p.2
Full source 
lemma continuous_nndist : Continuous fun p : α × α => nndist p.1 p.2 :=
  uniformContinuous_nndist.continuous
Continuity of Non-Negative Distance Function in Pseudometric Spaces
Informal description
For any pseudometric space $\alpha$, the non-negative distance function $\text{nndist} \colon \alpha \times \alpha \to \mathbb{R}_{\geq 0}$ is continuous, where $\alpha \times \alpha$ is equipped with the product topology.
Continuous.nndist theorem
[TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) : Continuous fun b => nndist (f b) (g b)
Full source 
@[fun_prop]
protected lemma Continuous.nndist [TopologicalSpace β] {f g : β → α} (hf : Continuous f)
    (hg : Continuous g) : Continuous fun b => nndist (f b) (g b) :=
  continuous_nndist.comp₂ hf hg
Continuity of Non-Negative Distance Between Continuous Functions
Informal description
Let $\alpha$ be a pseudometric space and $\beta$ be a topological space. For any two continuous functions $f, g \colon \beta \to \alpha$, the function $b \mapsto \text{nndist}(f(b), g(b))$ from $\beta$ to $\mathbb{R}_{\geq 0}$ is continuous, where $\text{nndist}$ denotes the non-negative distance function on $\alpha$.
Filter.Tendsto.nndist theorem
{f g : β → α} {x : Filter β} {a b : α} (hf : Tendsto f x (𝓝 a)) (hg : Tendsto g x (𝓝 b)) : Tendsto (fun x => nndist (f x) (g x)) x (𝓝 (nndist a b))
Full source 
protected lemma Filter.Tendsto.nndist {f g : β → α} {x : Filter β} {a b : α}
    (hf : Tendsto f x (𝓝 a)) (hg : Tendsto g x (𝓝 b)) :
    Tendsto (fun x => nndist (f x) (g x)) x (𝓝 (nndist a b)) :=
  (continuous_nndist.tendsto (a, b)).comp (hf.prodMk_nhds hg)
Limit of Non-Negative Distance Function under Convergent Functions
Informal description
Let $\alpha$ be a pseudometric space and $\beta$ be a topological space. For any functions $f, g \colon \beta \to \alpha$ and a filter $x$ on $\beta$, if $f$ tends to $a \in \alpha$ along $x$ and $g$ tends to $b \in \alpha$ along $x$, then the non-negative distance function $\text{nndist}(f(x), g(x))$ tends to $\text{nndist}(a, b)$ along $x$.