Mathlib.Topology.MetricSpace.Pseudo.Defs

UniformSpace.ofDist_aux theorem

(ε : ℝ) (hε : 0 < ε) : ∃ δ > (0 : ℝ), ∀ x < δ, ∀ y < δ, x + y < ε

Full source

theorem UniformSpace.ofDist_aux (ε : ℝ) (hε : 0 < ε) : ∃ δ > (0 : ℝ), ∀ x < δ, ∀ y < δ, x + y < ε :=
  ⟨ε / 2, half_pos hε, fun _x hx _y hy => add_halves ε ▸ add_lt_add hx hy⟩

Existence of $\delta$ for Sum Control in Uniform Space Construction

Informal description

For any positive real number $\varepsilon > 0$, there exists a positive real number $\delta > 0$ such that for any two real numbers $x, y$ with $x < \delta$ and $y < \delta$, their sum satisfies $x + y < \varepsilon$.

UniformSpace.ofDist definition

 (dist : α → α → ℝ) (dist_self : ∀ x : α, dist x x = 0) (dist_comm : ∀ x y : α, dist x y = dist y x)
  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : UniformSpace α

Full source

/-- Construct a uniform structure from a distance function and metric space axioms -/
def UniformSpace.ofDist (dist : α → α → ℝ) (dist_self : ∀ x : α, dist x x = 0)
    (dist_comm : ∀ x y : α, dist x y = dist y x)
    (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) : UniformSpace α :=
  .ofFun dist dist_self dist_comm dist_triangle ofDist_aux

Uniform space construction from a distance function

Informal description

Given a type $\alpha$ and a distance function $\mathrm{dist} : \alpha \to \alpha \to \mathbb{R}$ satisfying: 1. **Reflexivity**: $\mathrm{dist}(x, x) = 0$ for all $x \in \alpha$, 2. **Symmetry**: $\mathrm{dist}(x, y) = \mathrm{dist}(y, x)$ for all $x, y \in \alpha$, 3. **Triangle inequality**: $\mathrm{dist}(x, z) \leq \mathrm{dist}(x, y) + \mathrm{dist}(y, z)$ for all $x, y, z \in \alpha$, the function `UniformSpace.ofDist` constructs a uniform space structure on $\alpha$ where the uniformity is generated by the sets $\{(x, y) \mid \mathrm{dist}(x, y) < r\}$ for $r > 0$.

Bornology.ofDist abbrev

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

Full source

/-- Construct a bornology from a distance function and metric space axioms. -/
abbrev Bornology.ofDist {α : Type*} (dist : α → α → ℝ) (dist_comm : ∀ x y, dist x y = dist y x)
    (dist_triangle : ∀ x y z, dist x z ≤ dist x y + dist y z) : Bornology α :=
  Bornology.ofBounded { s : Set α | ∃ C, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C }
    ⟨0, fun _ hx _ => hx.elim⟩ (fun _ ⟨c, hc⟩ _ h => ⟨c, fun _ hx _ hy => hc (h hx) (h hy)⟩)
    (fun s hs t ht => by
      rcases s.eq_empty_or_nonempty with rfl | ⟨x, hx⟩
      · rwa [empty_union]
      rcases t.eq_empty_or_nonempty with rfl | ⟨y, hy⟩
      · rwa [union_empty]
      rsuffices ⟨C, hC⟩ : ∃ C, ∀ z ∈ s ∪ t, dist x z ≤ C
      · refine ⟨C + C, fun a ha b hb => (dist_triangle a x b).trans ?_⟩
        simpa only [dist_comm] using add_le_add (hC _ ha) (hC _ hb)
      rcases hs with ⟨Cs, hs⟩; rcases ht with ⟨Ct, ht⟩
      refine ⟨max Cs (dist x y + Ct), fun z hz => hz.elim
        (fun hz => (hs hx hz).trans (le_max_left _ _))
        (fun hz => (dist_triangle x y z).trans <|
          (add_le_add le_rfl (ht hy hz)).trans (le_max_right _ _))⟩)
    fun z => ⟨dist z z, forall_eq.2 <| forall_eq.2 le_rfl⟩

Construction of a Bornology from a Symmetric and Triangle-Inequality-Satisfying Distance Function

Informal description

Given a type $\alpha$ equipped with a distance function $\mathrm{dist} : \alpha \to \alpha \to \mathbb{R}$ that is symmetric (i.e., $\mathrm{dist}(x, y) = \mathrm{dist}(y, x)$ for all $x, y \in \alpha$) and satisfies the triangle inequality (i.e., $\mathrm{dist}(x, z) \leq \mathrm{dist}(x, y) + \mathrm{dist}(y, z)$ for all $x, y, z \in \alpha$), the function `Bornology.ofDist` constructs a bornology on $\alpha$. This bornology is defined such that a set is bounded if it is contained in a metric ball of finite radius.

Dist structure

(α : Type*)

Full source

/-- The distance function (given an ambient metric space on `α`), which returns
  a nonnegative real number `dist x y` given `x y : α`. -/
@[ext]
class Dist (α : Type*) where
  /-- Distance between two points -/
  dist : α → α → ℝ

Distance function on a space

Informal description

The typeclass `Dist α` endows a space `α` with a distance function `dist : α → α → ℝ` that measures the distance between any two points in `α`. This function is nonnegative and satisfies the following properties: 1. Reflexivity: `dist x x = 0` for all `x ∈ α`. 2. Symmetry: `dist x y = dist y x` for all `x, y ∈ α`. 3. Triangle inequality: `dist x z ≤ dist x y + dist y z` for all `x, y, z ∈ α`.

PseudoMetricSpace structure

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

Full source

/-- A pseudometric space is a type endowed with a `ℝ`-valued distance `dist` satisfying
reflexivity `dist x x = 0`, commutativity `dist x y = dist y x`, and the triangle inequality
`dist x z ≤ dist x y + dist y z`.

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

Any pseudometric 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 pseudometric space is just a 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
`[PseudoMetricSpace α] [PseudoMetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance]. -/
class PseudoMetricSpace (α : Type u) : Type u extends Dist α where
  dist_self : ∀ x : α, dist x x = 0
  dist_comm : ∀ x y : α, dist x y = dist y x
  dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z
  /-- Extended distance between two points -/
  edist : α → α → ℝ≥0∞ := fun x y => ENNReal.ofNNReal ⟨dist x y, dist_nonneg' _ ‹_› ‹_› ‹_›⟩
  edist_dist : ∀ x y : α, edist x y = ENNReal.ofReal (dist x y) := by
    intros x y; exact ENNReal.coe_nnreal_eq _
  toUniformSpace : UniformSpace α := .ofDist dist dist_self dist_comm dist_triangle
  uniformity_dist : 𝓤 α = ⨅ ε > 0, 𝓟 { p : α × α | dist p.1 p.2 < ε } := by intros; rfl
  toBornology : Bornology α := Bornology.ofDist dist dist_comm dist_triangle
  cobounded_sets : (Bornology.cobounded α).sets =
    { s | ∃ C : ℝ, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C } := by intros; rfl

Pseudometric space

Informal description

A pseudometric space is a type $\alpha$ equipped with a distance function $\text{dist} : \alpha \times \alpha \to \mathbb{R}$ satisfying the following properties: 1. Reflexivity: $\text{dist}(x, x) = 0$ for all $x \in \alpha$. 2. Symmetry: $\text{dist}(x, y) = \text{dist}(y, x)$ for all $x, y \in \alpha$. 3. Triangle inequality: $\text{dist}(x, z) \leq \text{dist}(x, y) + \text{dist}(y, z)$ for all $x, y, z \in \alpha$. Note that unlike a metric space, we do not require that $\text{dist}(x, y) = 0$ implies $x = y$. Every pseudometric space naturally induces a topology and a uniform structure.

PseudoMetricSpace.ext theorem

{α : Type*} {m m' : PseudoMetricSpace α} (h : m.toDist = m'.toDist) : m = m'

Full source

/-- Two pseudo metric space structures with the same distance function coincide. -/
@[ext]
theorem PseudoMetricSpace.ext {α : Type*} {m m' : PseudoMetricSpace α}
    (h : m.toDist = m'.toDist) : m = m' := by
  let d := m.toDist
  obtain ⟨_, _, _, _, hed, _, hU, _, hB⟩ := m
  let d' := m'.toDist
  obtain ⟨_, _, _, _, hed', _, hU', _, hB'⟩ := m'
  obtain rfl : d = d' := h
  congr
  · ext x y : 2
    rw [hed, hed']
  · exact UniformSpace.ext (hU.trans hU'.symm)
  · ext : 2
    rw [← Filter.mem_sets, ← Filter.mem_sets, hB, hB']

Uniqueness of Pseudometric Space Structure via Distance Function

Informal description

Let $\alpha$ be a type, and let $m$ and $m'$ be two pseudometric space structures on $\alpha$. If the distance functions associated with $m$ and $m'$ are equal, i.e., $m.\text{toDist} = m'.\text{toDist}$, then the pseudometric space structures $m$ and $m'$ are identical.

PseudoMetricSpace.toEDist instance

: EDist α

Full source

instance (priority := 200) PseudoMetricSpace.toEDist : EDist α :=
  ⟨PseudoMetricSpace.edist⟩

Extended Distance Function on Pseudometric Spaces

Informal description

Every pseudometric space $\alpha$ is naturally endowed with an extended distance function $\text{edist} : \alpha \times \alpha \to \mathbb{R}_{\geq 0} \cup \{\infty\}$.

PseudoMetricSpace.ofDistTopology definition

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

Full source

/-- Construct a pseudo-metric space structure whose underlying topological space structure
(definitionally) agrees which a pre-existing topology which is compatible with a given distance
function. -/
def PseudoMetricSpace.ofDistTopology {α : Type u} [TopologicalSpace α] (dist : α → α → ℝ)
    (dist_self : ∀ x : α, dist x x = 0) (dist_comm : ∀ x y : α, dist x y = dist y x)
    (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
    (H : ∀ s : Set α, IsOpenIsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ y, dist x y < ε → y ∈ s) :
    PseudoMetricSpace α :=
  { dist := dist
    dist_self := dist_self
    dist_comm := dist_comm
    dist_triangle := dist_triangle
    toUniformSpace :=
      (UniformSpace.ofDist dist dist_self dist_comm dist_triangle).replaceTopology <|
        TopologicalSpace.ext_iff.2 fun s ↦ (H s).trans <| forall₂_congr fun x _ ↦
          ((UniformSpace.hasBasis_ofFun (exists_gt (0 : ℝ)) dist dist_self dist_comm dist_triangle
            UniformSpace.ofDist_aux).comap (Prod.mk x)).mem_iff.symm
    uniformity_dist := rfl
    toBornology := Bornology.ofDist dist dist_comm dist_triangle
    cobounded_sets := rfl }

Pseudometric space construction from a distance function compatible with a given topology

Informal description

Given a type $\alpha$ with a topological space structure, a distance function $\text{dist} : \alpha \times \alpha \to \mathbb{R}$ satisfying: 1. Reflexivity: $\text{dist}(x, x) = 0$ for all $x \in \alpha$, 2. Symmetry: $\text{dist}(x, y) = \text{dist}(y, x)$ for all $x, y \in \alpha$, 3. Triangle inequality: $\text{dist}(x, z) \leq \text{dist}(x, y) + \text{dist}(y, z)$ for all $x, y, z \in \alpha$, and the condition that the topology is induced by the distance function (i.e., a set $s \subseteq \alpha$ is open if and only if for every $x \in s$ there exists $\epsilon > 0$ such that the ball $\{y \mid \text{dist}(x, y) < \epsilon\}$ is contained in $s$), this constructs a pseudometric space structure on $\alpha$ whose underlying topology agrees with the given one.

dist_self theorem

(x : α) : dist x x = 0

Full source

@[simp]
theorem dist_self (x : α) : dist x x = 0 :=
  PseudoMetricSpace.dist_self x

Reflexivity of the Distance Function in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, the distance from any point $x \in \alpha$ to itself is zero, i.e., $\text{dist}(x, x) = 0$.

dist_comm theorem

(x y : α) : dist x y = dist y x

Full source

theorem dist_comm (x y : α) : dist x y = dist y x :=
  PseudoMetricSpace.dist_comm x y

Symmetry of the Distance Function in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, the distance function $\text{dist} : \alpha \times \alpha \to \mathbb{R}$ is symmetric, i.e., for any two points $x, y \in \alpha$, we have $\text{dist}(x, y) = \text{dist}(y, x)$.

edist_dist theorem

(x y : α) : edist x y = ENNReal.ofReal (dist x y)

Full source

theorem edist_dist (x y : α) : edist x y = ENNReal.ofReal (dist x y) :=
  PseudoMetricSpace.edist_dist x y

Extended Distance as Nonnegative Embedding of Distance

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the extended distance $\text{edist}(x, y)$ is equal to the embedding of the distance $\text{dist}(x, y)$ into the extended nonnegative real numbers, i.e., $\text{edist}(x, y) = \max(\text{dist}(x, y), 0)$.

dist_triangle theorem

(x y z : α) : dist x z ≤ dist x y + dist y z

Full source

@[bound]
theorem dist_triangle (x y z : α) : dist x z ≤ dist x y + dist y z :=
  PseudoMetricSpace.dist_triangle x y z

Triangle Inequality in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, the distance function $\text{dist} : \alpha \times \alpha \to \mathbb{R}$ satisfies the triangle inequality: for any three points $x, y, z \in \alpha$, we have $\text{dist}(x, z) \leq \text{dist}(x, y) + \text{dist}(y, z)$.

dist_triangle_left theorem

(x y z : α) : dist x y ≤ dist z x + dist z y

Full source

theorem dist_triangle_left (x y z : α) : dist x y ≤ dist z x + dist z y := by
  rw [dist_comm z]; apply dist_triangle

Left Triangle Inequality in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, for any three points $x, y, z \in \alpha$, the distance function satisfies the left triangle inequality: \[ \text{dist}(x, y) \leq \text{dist}(z, x) + \text{dist}(z, y). \]

dist_triangle_right theorem

(x y z : α) : dist x y ≤ dist x z + dist y z

Full source

theorem dist_triangle_right (x y z : α) : dist x y ≤ dist x z + dist y z := by
  rw [dist_comm y]; apply dist_triangle

Right Triangle Inequality in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, for any three points $x, y, z \in \alpha$, the distance function satisfies the right triangle inequality: \[ \text{dist}(x, y) \leq \text{dist}(x, z) + \text{dist}(y, z). \]

dist_triangle4 theorem

(x y z w : α) : dist x w ≤ dist x y + dist y z + dist z w

Full source

theorem dist_triangle4 (x y z w : α) : dist x w ≤ dist x y + dist y z + dist z w :=
  calc
    dist x w ≤ dist x z + dist z w := dist_triangle x z w
    _ ≤ dist x y + dist y z + dist z w := add_le_add_right (dist_triangle x y z) _

Four-Point Triangle Inequality in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, for any four points $x, y, z, w \in \alpha$, the distance function satisfies the four-point triangle inequality: \[ \text{dist}(x, w) \leq \text{dist}(x, y) + \text{dist}(y, z) + \text{dist}(z, w). \]

dist_triangle4_left theorem

(x₁ y₁ x₂ y₂ : α) : dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)

Full source

theorem dist_triangle4_left (x₁ y₁ x₂ y₂ : α) :
    dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂) := by
  rw [add_left_comm, dist_comm x₁, ← add_assoc]
  apply dist_triangle4

Left Four-Point Triangle Inequality in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, for any four points $x₁, y₁, x₂, y₂ \in \alpha$, the distance function satisfies the following inequality: \[ \text{dist}(x₂, y₂) \leq \text{dist}(x₁, y₁) + (\text{dist}(x₁, x₂) + \text{dist}(y₁, y₂)). \]

dist_triangle4_right theorem

(x₁ y₁ x₂ y₂ : α) : dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂

Full source

theorem dist_triangle4_right (x₁ y₁ x₂ y₂ : α) :
    dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂ := by
  rw [add_right_comm, dist_comm y₁]
  apply dist_triangle4

Right Four-Point Triangle Inequality in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, for any four points $x₁, y₁, x₂, y₂ \in \alpha$, the distance function satisfies the inequality: \[ \text{dist}(x₁, y₁) \leq \text{dist}(x₁, x₂) + \text{dist}(y₁, y₂) + \text{dist}(x₂, y₂). \]

dist_triangle8 theorem

(a b c d e f g h : α) : dist a h ≤ dist a b + dist b c + dist c d + dist d e + dist e f + dist f g + dist g h

Full source

theorem dist_triangle8 (a b c d e f g h : α) : dist a h ≤ dist a b + dist b c + dist c d
    + dist d e + dist e f + dist f g + dist g h := by
  apply le_trans (dist_triangle4 a f g h)
  apply add_le_add_right (add_le_add_right _ (dist f g)) (dist g h)
  apply le_trans (dist_triangle4 a d e f)
  apply add_le_add_right (add_le_add_right _ (dist d e)) (dist e f)
  exact dist_triangle4 a b c d

Eight-Point Triangle Inequality in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, for any eight points $a, b, c, d, e, f, g, h \in \alpha$, the distance function satisfies the eight-point triangle inequality: \[ \text{dist}(a, h) \leq \text{dist}(a, b) + \text{dist}(b, c) + \text{dist}(c, d) + \text{dist}(d, e) + \text{dist}(e, f) + \text{dist}(f, g) + \text{dist}(g, h). \]

swap_dist theorem

: Function.swap (@dist α _) = dist

Full source

theorem swap_dist : Function.swap (@dist α _) = dist := by funext x y; exact dist_comm _ _

Equality of Swapped and Original Distance Functions in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, the swapped distance function $\operatorname{swap}(\text{dist})$ is equal to the original distance function $\text{dist}$, i.e., $\operatorname{swap}(\text{dist}) = \text{dist}$.

abs_dist_sub_le theorem

(x y z : α) : |dist x z - dist y z| ≤ dist x y

Full source

theorem abs_dist_sub_le (x y z : α) : |dist x z - dist y z| ≤ dist x y :=
  abs_sub_le_iff.2
    ⟨sub_le_iff_le_add.2 (dist_triangle _ _ _), sub_le_iff_le_add.2 (dist_triangle_left _ _ _)⟩

Reverse Triangle Inequality for Distances in Pseudometric Spaces

Informal description

For any three points $x, y, z$ in a pseudometric space $\alpha$, the absolute difference between the distances from $x$ to $z$ and from $y$ to $z$ is bounded by the distance between $x$ and $y$, i.e., \[ |\text{dist}(x, z) - \text{dist}(y, z)| \leq \text{dist}(x, y). \]

dist_nonneg theorem

{x y : α} : 0 ≤ dist x y

Full source

@[bound]
theorem dist_nonneg {x y : α} : 0 ≤ dist x y :=
  dist_nonneg' dist dist_self dist_comm dist_triangle

Nonnegativity of Distance in Pseudometric Spaces

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the distance between them is nonnegative, i.e., $\text{dist}(x, y) \geq 0$.

Mathlib.Meta.Positivity.evalDist definition

: PositivityExt

Full source

/-- Extension for the `positivity` tactic: distances are nonnegative. -/
@[positivity Dist.dist _ _]
def evalDist : PositivityExt where eval {u α} _zα _pα e := do
  match u, α, e with
  | 0, ~q(ℝ), ~q(@Dist.dist $β $inst $a $b) =>
    let _inst ← synthInstanceQ q(PseudoMetricSpace $β)
    assertInstancesCommute
    pure (.nonnegative q(dist_nonneg))
  | _, _, _ => throwError "not dist"

Nonnegativity of distance in pseudo-metric spaces

Informal description

The function `evalDist` is an extension for the `positivity` tactic, which asserts that distances in a pseudo-metric space are nonnegative. Specifically, for any elements `a` and `b` in a pseudo-metric space `β`, the distance `dist a b` is nonnegative.

abs_dist theorem

{a b : α} : |dist a b| = dist a b

Full source

@[simp] theorem abs_dist {a b : α} : |dist a b| = dist a b := abs_of_nonneg dist_nonneg

Absolute Value of Distance Equals Distance in Pseudometric Spaces

Informal description

For any two points $a$ and $b$ in a pseudometric space $\alpha$, the absolute value of the distance between them equals the distance itself, i.e., $|\text{dist}(a, b)| = \text{dist}(a, b)$.

NNDist structure

(α : Type*)

Full source

/-- A version of `Dist` that takes value in `ℝ≥0`. -/
class NNDist (α : Type*) where
  /-- Nonnegative distance between two points -/
  nndist : α → α → ℝ≥0

Non-negative distance function

Informal description

The structure `NNDist α` endows a space `α` with a distance function `dist a b` that takes values in the non-negative real numbers. This is a variant of the usual distance function where the codomain is restricted to `ℝ≥0`.

PseudoMetricSpace.toNNDist instance

: NNDist α

Full source

/-- Distance as a nonnegative real number. -/
instance (priority := 100) PseudoMetricSpace.toNNDist : NNDist α :=
  ⟨fun a b => ⟨dist a b, dist_nonneg⟩⟩

Non-negative Distance Function on Pseudometric Spaces

Informal description

Every pseudometric space $\alpha$ can be endowed with a non-negative distance function $\text{nndist} : \alpha \times \alpha \to \mathbb{R}_{\geq 0}$, where $\text{nndist}(x, y) = \text{dist}(x, y)$ for all $x, y \in \alpha$.

dist_nndist theorem

(x y : α) : dist x y = nndist x y

Full source

/-- Express `dist` in terms of `nndist` -/
theorem dist_nndist (x y : α) : dist x y = nndist x y := rfl

Distance Equals Non-negative Distance in Pseudometric Spaces

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the distance $\text{dist}(x, y)$ is equal to the non-negative distance $\text{nndist}(x, y)$.

coe_nndist theorem

(x y : α) : ↑(nndist x y) = dist x y

Full source

@[simp, norm_cast]
theorem coe_nndist (x y : α) : ↑(nndist x y) = dist x y := rfl

Equality of Coerced Non-Negative Distance and Standard Distance in Pseudometric Spaces

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the non-negative distance $\text{nndist}(x, y)$ between them, when coerced to a real number, equals the standard distance $\text{dist}(x, y)$. That is, $\text{nndist}(x, y) = \text{dist}(x, y)$.

edist_nndist theorem

(x y : α) : edist x y = nndist x y

Full source

/-- Express `edist` in terms of `nndist` -/
theorem edist_nndist (x y : α) : edist x y = nndist x y := by
  rw [edist_dist, dist_nndist, ENNReal.ofReal_coe_nnreal]

Extended Distance Equals Non-negative Distance in Pseudometric Spaces

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the extended distance $\text{edist}(x, y)$ is equal to the non-negative distance $\text{nndist}(x, y)$.

nndist_edist theorem

(x y : α) : nndist x y = (edist x y).toNNReal

Full source

/-- Express `nndist` in terms of `edist` -/
theorem nndist_edist (x y : α) : nndist x y = (edist x y).toNNReal := by
  simp [edist_nndist]

Non-negative Distance as Extended Distance Conversion: $\text{nndist}(x, y) = \text{toNNReal}(\text{edist}(x, y))$

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the non-negative distance $\text{nndist}(x, y)$ is equal to the extended distance $\text{edist}(x, y)$ converted to a non-negative real number via the function $\text{toNNReal}$. That is, $\text{nndist}(x, y) = \text{toNNReal}(\text{edist}(x, y))$.

coe_nnreal_ennreal_nndist theorem

(x y : α) : ↑(nndist x y) = edist x y

Full source

@[simp, norm_cast]
theorem coe_nnreal_ennreal_nndist (x y : α) : ↑(nndist x y) = edist x y :=
  (edist_nndist x y).symm

Embedding of Non-negative Distance into Extended Distance

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the extended distance $\text{edist}(x, y)$ is equal to the canonical embedding of the non-negative distance $\text{nndist}(x, y)$ into the extended non-negative real numbers, i.e., $\text{edist}(x, y) = \text{nndist}(x, y)$.

edist_lt_coe theorem

{x y : α} {c : ℝ≥0} : edist x y < c ↔ nndist x y < c

Full source

@[simp, norm_cast]
theorem edist_lt_coe {x y : α} {c : ℝ≥0} : edistedist x y < c ↔ nndist x y < c := by
  rw [edist_nndist, ENNReal.coe_lt_coe]

Extended Distance vs Nonnegative Distance Strict Inequality

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$ and any nonnegative real number $c$, the extended distance $\text{edist}(x, y)$ is strictly less than $c$ if and only if the nonnegative distance $\text{nndist}(x, y)$ is strictly less than $c$.

edist_le_coe theorem

{x y : α} {c : ℝ≥0} : edist x y ≤ c ↔ nndist x y ≤ c

Full source

@[simp, norm_cast]
theorem edist_le_coe {x y : α} {c : ℝ≥0} : edistedist x y ≤ c ↔ nndist x y ≤ c := by
  rw [edist_nndist, ENNReal.coe_le_coe]

Extended Distance Bounded by Nonnegative Real if and only if Non-negative Distance is Bounded

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$ and any nonnegative real number $c$, the extended distance $\text{edist}(x, y)$ is less than or equal to $c$ if and only if the non-negative distance $\text{nndist}(x, y)$ is less than or equal to $c$.

edist_lt_top theorem

{α : Type*} [PseudoMetricSpace α] (x y : α) : edist x y < ⊤

Full source

/-- In a pseudometric space, the extended distance is always finite -/
theorem edist_lt_top {α : Type*} [PseudoMetricSpace α] (x y : α) : edist x y < ⊤ :=
  (edist_dist x y).symm ▸ ENNReal.ofReal_lt_top

Extended Distance is Finite in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, the extended distance between any two points $x$ and $y$ is always finite, i.e., $\text{edist}(x, y) < \infty$.

edist_ne_top theorem

(x y : α) : edist x y ≠ ⊤

Full source

/-- In a pseudometric space, the extended distance is always finite -/
theorem edist_ne_top (x y : α) : edistedist x y ≠ ⊤ :=
  (edist_lt_top x y).ne

Extended Distance is Finite in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, the extended distance between any two points $x$ and $y$ is not equal to infinity, i.e., $\text{edist}(x, y) \neq \infty$.

nndist_self theorem

(a : α) : nndist a a = 0

Full source

/-- `nndist x x` vanishes -/
@[simp] theorem nndist_self (a : α) : nndist a a = 0 := NNReal.coe_eq_zero.1 (dist_self a)

Reflexivity of Non-Negative Distance Function in Pseudometric Spaces

Informal description

For any point $a$ in a pseudometric space $\alpha$, the non-negative distance from $a$ to itself is zero, i.e., $\text{nndist}(a, a) = 0$.

dist_lt_coe theorem

{x y : α} {c : ℝ≥0} : dist x y < c ↔ nndist x y < c

Full source

@[simp, norm_cast]
theorem dist_lt_coe {x y : α} {c : ℝ≥0} : distdist x y < c ↔ nndist x y < c :=
  Iff.rfl

Equivalence of Distance and Non-Negative Distance Bounds: $\text{dist}(x, y) < c \leftrightarrow \text{nndist}(x, y) < c$

Informal description

For any two points $x, y$ in a pseudometric space $\alpha$ and any non-negative real number $c$, the distance between $x$ and $y$ is less than $c$ if and only if the non-negative distance between $x$ and $y$ is less than $c$. In other words, $\text{dist}(x, y) < c \leftrightarrow \text{nndist}(x, y) < c$.

dist_le_coe theorem

{x y : α} {c : ℝ≥0} : dist x y ≤ c ↔ nndist x y ≤ c

Full source

@[simp, norm_cast]
theorem dist_le_coe {x y : α} {c : ℝ≥0} : distdist x y ≤ c ↔ nndist x y ≤ c :=
  Iff.rfl

Distance and Non-negative Distance Inequality Equivalence

Informal description

For any points $x, y$ in a pseudometric space $\alpha$ and any non-negative real number $c$, the distance $\text{dist}(x, y)$ is less than or equal to $c$ if and only if the non-negative distance $\text{nndist}(x, y)$ is less than or equal to $c$.

edist_lt_ofReal theorem

{x y : α} {r : ℝ} : edist x y < ENNReal.ofReal r ↔ dist x y < r

Full source

@[simp]
theorem edist_lt_ofReal {x y : α} {r : ℝ} : edistedist x y < ENNReal.ofReal r ↔ dist x y < r := by
  rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg]

Extended Distance Strict Inequality Characterization via Real Embedding

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$ and any real number $r$, the extended distance $\text{edist}(x, y)$ is less than the embedding of $r$ into the extended nonnegative real numbers if and only if the distance $\text{dist}(x, y)$ is less than $r$. That is, $\text{edist}(x, y) < [r] \leftrightarrow \text{dist}(x, y) < r$, where $[r] = \max(r, 0)$.

edist_le_ofReal theorem

{x y : α} {r : ℝ} (hr : 0 ≤ r) : edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r

Full source

@[simp]
theorem edist_le_ofReal {x y : α} {r : ℝ} (hr : 0 ≤ r) :
    edistedist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r := by
  rw [edist_dist, ENNReal.ofReal_le_ofReal_iff hr]

Extended Distance Bound via Real Distance

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$ and any nonnegative real number $r \geq 0$, the extended distance $\text{edist}(x, y)$ is less than or equal to the embedding of $r$ into the extended nonnegative reals if and only if the distance $\text{dist}(x, y)$ is less than or equal to $r$. In symbols: \[ \text{edist}(x, y) \leq \text{ENNReal.ofReal}(r) \leftrightarrow \text{dist}(x, y) \leq r \]

nndist_dist theorem

(x y : α) : nndist x y = Real.toNNReal (dist x y)

Full source

/-- Express `nndist` in terms of `dist` -/
theorem nndist_dist (x y : α) : nndist x y = Real.toNNReal (dist x y) := by
  rw [dist_nndist, Real.toNNReal_coe]

Non-negative Distance as Real-to-NNReal of Distance

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the non-negative distance $\text{nndist}(x, y)$ is equal to the canonical embedding of the distance $\text{dist}(x, y)$ into the non-negative real numbers via the function $\text{Real.toNNReal}$. That is: \[ \text{nndist}(x, y) = \text{Real.toNNReal}(\text{dist}(x, y)) \]

nndist_comm theorem

(x y : α) : nndist x y = nndist y x

Full source

theorem nndist_comm (x y : α) : nndist x y = nndist y x := NNReal.eq <| dist_comm x y

Symmetry of Non-Negative Distance in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, the non-negative distance function $\text{nndist} : \alpha \times \alpha \to \mathbb{R}_{\geq 0}$ is symmetric, i.e., for any two points $x, y \in \alpha$, we have $\text{nndist}(x, y) = \text{nndist}(y, x)$.

nndist_triangle theorem

(x y z : α) : nndist x z ≤ nndist x y + nndist y z

Full source

/-- Triangle inequality for the nonnegative distance -/
theorem nndist_triangle (x y z : α) : nndist x z ≤ nndist x y + nndist y z :=
  dist_triangle _ _ _

Triangle Inequality for Non-Negative Distance in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, the non-negative distance function $\text{nndist} : \alpha \times \alpha \to \mathbb{R}_{\geq 0}$ satisfies the triangle inequality: for any three points $x, y, z \in \alpha$, we have $\text{nndist}(x, z) \leq \text{nndist}(x, y) + \text{nndist}(y, z)$.

nndist_triangle_left theorem

(x y z : α) : nndist x y ≤ nndist z x + nndist z y

Full source

theorem nndist_triangle_left (x y z : α) : nndist x y ≤ nndist z x + nndist z y :=
  dist_triangle_left _ _ _

Left Triangle Inequality for Non-Negative Distance in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, for any three points $x, y, z \in \alpha$, the non-negative distance function satisfies the left triangle inequality: \[ \text{nndist}(x, y) \leq \text{nndist}(z, x) + \text{nndist}(z, y). \]

nndist_triangle_right theorem

(x y z : α) : nndist x y ≤ nndist x z + nndist y z

Full source

theorem nndist_triangle_right (x y z : α) : nndist x y ≤ nndist x z + nndist y z :=
  dist_triangle_right _ _ _

Right Triangle Inequality for Non-Negative Distance in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, for any three points $x, y, z \in \alpha$, the non-negative distance function satisfies the right triangle inequality: \[ \text{nndist}(x, y) \leq \text{nndist}(x, z) + \text{nndist}(y, z). \]

dist_edist theorem

(x y : α) : dist x y = (edist x y).toReal

Full source

/-- Express `dist` in terms of `edist` -/
theorem dist_edist (x y : α) : dist x y = (edist x y).toReal := by
  rw [edist_dist, ENNReal.toReal_ofReal dist_nonneg]

Distance as Real Part of Extended Distance

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, the distance $\text{dist}(x, y)$ is equal to the real part of the extended distance $\text{edist}(x, y)$, i.e., $\text{dist}(x, y) = \text{toReal}(\text{edist}(x, y))$.

Metric.ball definition

(x : α) (ε : ℝ) : Set α

Full source

/-- `ball x ε` is the set of all points `y` with `dist y x < ε` -/
def ball (x : α) (ε : ℝ) : Set α :=
  { y | dist y x < ε }

Open ball in a pseudometric space

Informal description

For a point $x$ in a pseudometric space $\alpha$ and a positive real number $\varepsilon$, the open ball $\text{ball}(x, \varepsilon)$ is the set of all points $y \in \alpha$ such that the distance between $y$ and $x$ is less than $\varepsilon$, i.e., $\text{ball}(x, \varepsilon) = \{ y \mid \text{dist}(y, x) < \varepsilon \}$.

Metric.mem_ball theorem

: y ∈ ball x ε ↔ dist y x < ε

Full source

@[simp]
theorem mem_ball : y ∈ ball x εy ∈ ball x ε ↔ dist y x < ε :=
  Iff.rfl

Characterization of Open Ball Membership via Distance

Informal description

For any points $x$ and $y$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon$, the point $y$ belongs to the open ball centered at $x$ with radius $\varepsilon$ if and only if the distance from $y$ to $x$ is strictly less than $\varepsilon$, i.e., $y \in \text{ball}(x, \varepsilon) \leftrightarrow \text{dist}(y, x) < \varepsilon$.

Metric.mem_ball' theorem

: y ∈ ball x ε ↔ dist x y < ε

Full source

theorem mem_ball' : y ∈ ball x εy ∈ ball x ε ↔ dist x y < ε := by rw [dist_comm, mem_ball]

Characterization of Open Ball Membership via Symmetric Distance

Informal description

For any points $x$ and $y$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon$, the point $y$ belongs to the open ball centered at $x$ with radius $\varepsilon$ if and only if the distance from $x$ to $y$ is strictly less than $\varepsilon$, i.e., $y \in \text{ball}(x, \varepsilon) \leftrightarrow \text{dist}(x, y) < \varepsilon$.

Metric.pos_of_mem_ball theorem

(hy : y ∈ ball x ε) : 0 < ε

Full source

theorem pos_of_mem_ball (hy : y ∈ ball x ε) : 0 < ε :=
  dist_nonneg.trans_lt hy

Positivity of Radius in Open Ball Membership

Informal description

For any points $x$ and $y$ in a pseudometric space $\alpha$ and any $\varepsilon > 0$, if $y$ belongs to the open ball centered at $x$ with radius $\varepsilon$, then $\varepsilon$ must be positive, i.e., $y \in \text{ball}(x, \varepsilon) \implies \varepsilon > 0$.

Metric.mem_ball_self theorem

(h : 0 < ε) : x ∈ ball x ε

Full source

theorem mem_ball_self (h : 0 < ε) : x ∈ ball x ε := by
  rwa [mem_ball, dist_self]

Every Point Belongs to Its Own Open Ball in a Pseudometric Space

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon > 0$, the point $x$ belongs to the open ball centered at $x$ with radius $\varepsilon$, i.e., $x \in \text{ball}(x, \varepsilon)$.

Metric.nonempty_ball theorem

: (ball x ε).Nonempty ↔ 0 < ε

Full source

@[simp]
theorem nonempty_ball : (ball x ε).Nonempty ↔ 0 < ε :=
  ⟨fun ⟨_x, hx⟩ => pos_of_mem_ball hx, fun h => ⟨x, mem_ball_self h⟩⟩

Nonempty Open Ball Condition: $\text{ball}(x, \varepsilon) \neq \emptyset \iff \varepsilon > 0$

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $\varepsilon$, the open ball $\text{ball}(x, \varepsilon)$ is nonempty if and only if $\varepsilon > 0$.

Metric.ball_eq_empty theorem

: ball x ε = ∅ ↔ ε ≤ 0

Full source

@[simp]
theorem ball_eq_empty : ballball x ε = ∅ ↔ ε ≤ 0 := by
  rw [← not_nonempty_iff_eq_empty, nonempty_ball, not_lt]

Empty Ball Condition: $\text{ball}(x, \varepsilon) = \emptyset \iff \varepsilon \leq 0$

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $\varepsilon$, the open ball $\text{ball}(x, \varepsilon)$ is empty if and only if $\varepsilon \leq 0$.

Metric.ball_zero theorem

: ball x 0 = ∅

Full source

@[simp]
theorem ball_zero : ball x 0 = ∅ := by rw [ball_eq_empty]

Open Ball with Zero Radius is Empty

Informal description

For any point $x$ in a pseudometric space $\alpha$, the open ball centered at $x$ with radius $0$ is empty, i.e., $\text{ball}(x, 0) = \emptyset$.

Metric.exists_lt_mem_ball_of_mem_ball theorem

(h : x ∈ ball y ε) : ∃ ε' < ε, x ∈ ball y ε'

Full source

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

See also `exists_lt_subset_ball`. -/
theorem exists_lt_mem_ball_of_mem_ball (h : x ∈ ball y ε) : ∃ ε' < ε, x ∈ ball y ε' := by
  simp only [mem_ball] at h ⊢
  exact ⟨(dist x y + ε) / 2, by linarith, by linarith⟩

Existence of Strictly Smaller Radius for Points in Open Balls

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon$, if $x$ belongs to the open ball centered at $y$ with radius $\varepsilon$, then there exists a strictly smaller radius $\varepsilon' < \varepsilon$ such that $x$ still belongs to the open ball centered at $y$ with radius $\varepsilon'$.

Metric.ball_eq_ball theorem

(ε : ℝ) (x : α) : UniformSpace.ball x {p | dist p.2 p.1 < ε} = Metric.ball x ε

Full source

theorem ball_eq_ball (ε : ℝ) (x : α) :
    UniformSpace.ball x { p | dist p.2 p.1 < ε } = Metric.ball x ε :=
  rfl

Equality of Uniform Ball and Metric Ball with Reversed Arguments

Informal description

For any real number $\varepsilon$ and any point $x$ in a pseudometric space $\alpha$, the uniform ball centered at $x$ with respect to the entourage $\{(a, b) \mid \text{dist}(b, a) < \varepsilon\}$ is equal to the metric ball $\text{ball}(x, \varepsilon)$.

Metric.ball_eq_ball' theorem

(ε : ℝ) (x : α) : UniformSpace.ball x {p | dist p.1 p.2 < ε} = Metric.ball x ε

Full source

theorem ball_eq_ball' (ε : ℝ) (x : α) :
    UniformSpace.ball x { p | dist p.1 p.2 < ε } = Metric.ball x ε := by
  ext
  simp [dist_comm, UniformSpace.ball]

Equality of Uniform Ball and Metric Ball via Distance Condition

Informal description

For any real number $\varepsilon > 0$ and any point $x$ in a pseudometric space $\alpha$, the uniform ball centered at $x$ with respect to the entourage $\{(a, b) \mid \text{dist}(a, b) < \varepsilon\}$ is equal to the metric ball $\text{ball}(x, \varepsilon)$.

Metric.iUnion_ball_nat theorem

(x : α) : ⋃ n : ℕ, ball x n = univ

Full source

@[simp]
theorem iUnion_ball_nat (x : α) : ⋃ n : ℕ, ball x n = univ :=
  iUnion_eq_univ_iff.2 fun y => exists_nat_gt (dist y x)

Union of Expanding Balls Covers the Space

Informal description

For any point $x$ in a pseudometric space $\alpha$, the union of open balls centered at $x$ with radii $n$ over all natural numbers $n$ equals the universal set of $\alpha$. In other words, $\bigcup_{n \in \mathbb{N}} B(x, n) = \alpha$.

Metric.iUnion_ball_nat_succ theorem

(x : α) : ⋃ n : ℕ, ball x (n + 1) = univ

Full source

@[simp]
theorem iUnion_ball_nat_succ (x : α) : ⋃ n : ℕ, ball x (n + 1) = univ :=
  iUnion_eq_univ_iff.2 fun y => (exists_nat_gt (dist y x)).imp fun _ h => h.trans (lt_add_one _)

Union of Expanding Balls with Successor Radii Covers the Space

Informal description

For any point $x$ in a pseudometric space $\alpha$, the union of open balls centered at $x$ with radii $n+1$ over all natural numbers $n$ equals the universal set of $\alpha$, i.e., $\bigcup_{n \in \mathbb{N}} B(x, n+1) = \alpha$.

Metric.closedBall definition

(x : α) (ε : ℝ)

Full source

/-- `closedBall x ε` is the set of all points `y` with `dist y x ≤ ε` -/
def closedBall (x : α) (ε : ℝ) :=
  { y | dist y x ≤ ε }

Closed ball in a pseudometric space

Informal description

For a point $x$ in a pseudometric space $\alpha$ and a non-negative real number $\varepsilon$, the closed ball $\overline{B}(x, \varepsilon)$ is the set of all points $y \in \alpha$ such that the distance from $y$ to $x$ is at most $\varepsilon$, i.e., $\overline{B}(x, \varepsilon) = \{ y \mid \text{dist}(y, x) \leq \varepsilon \}$.

Metric.mem_closedBall theorem

: y ∈ closedBall x ε ↔ dist y x ≤ ε

Full source

@[simp] theorem mem_closedBall : y ∈ closedBall x εy ∈ closedBall x ε ↔ dist y x ≤ ε := Iff.rfl

Characterization of Closed Ball Membership via Distance

Informal description

For any point $y$ in a pseudometric space $\alpha$, $y$ belongs to the closed ball $\overline{B}(x, \varepsilon)$ centered at $x$ with radius $\varepsilon$ if and only if the distance from $y$ to $x$ is at most $\varepsilon$, i.e., $y \in \overline{B}(x, \varepsilon) \leftrightarrow \text{dist}(y, x) \leq \varepsilon$.

Metric.mem_closedBall' theorem

: y ∈ closedBall x ε ↔ dist x y ≤ ε

Full source

theorem mem_closedBall' : y ∈ closedBall x εy ∈ closedBall x ε ↔ dist x y ≤ ε := by rw [dist_comm, mem_closedBall]

Closed Ball Membership via Symmetric Distance

Informal description

For any point $y$ in a pseudometric space $\alpha$, $y$ belongs to the closed ball $\overline{B}(x, \varepsilon)$ centered at $x$ with radius $\varepsilon$ if and only if the distance from $x$ to $y$ is at most $\varepsilon$, i.e., $y \in \overline{B}(x, \varepsilon) \leftrightarrow \text{dist}(x, y) \leq \varepsilon$.

Metric.sphere definition

(x : α) (ε : ℝ)

Full source

/-- `sphere x ε` is the set of all points `y` with `dist y x = ε` -/
def sphere (x : α) (ε : ℝ) := { y | dist y x = ε }

Sphere in a pseudometric space

Informal description

For a point $x$ in a pseudometric space $\alpha$ and a non-negative real number $\varepsilon$, the sphere $\text{sphere}(x, \varepsilon)$ is the set of all points $y \in \alpha$ such that the distance between $y$ and $x$ is exactly $\varepsilon$, i.e., $\text{dist}(y, x) = \varepsilon$.

Metric.mem_sphere theorem

: y ∈ sphere x ε ↔ dist y x = ε

Full source

@[simp] theorem mem_sphere : y ∈ sphere x εy ∈ sphere x ε ↔ dist y x = ε := Iff.rfl

Characterization of Sphere Membership via Distance

Informal description

For any point $y$ in a pseudometric space $\alpha$, $y$ belongs to the sphere centered at $x$ with radius $\varepsilon$ if and only if the distance from $y$ to $x$ equals $\varepsilon$, i.e., $y \in \text{sphere}(x, \varepsilon) \leftrightarrow \text{dist}(y, x) = \varepsilon$.

Metric.mem_sphere' theorem

: y ∈ sphere x ε ↔ dist x y = ε

Full source

theorem mem_sphere' : y ∈ sphere x εy ∈ sphere x ε ↔ dist x y = ε := by rw [dist_comm, mem_sphere]

Characterization of Sphere Membership via Symmetric Distance

Informal description

For any point $y$ in a pseudometric space $\alpha$, $y$ belongs to the sphere centered at $x$ with radius $\varepsilon$ if and only if the distance from $x$ to $y$ equals $\varepsilon$, i.e., $y \in \text{sphere}(x, \varepsilon) \leftrightarrow \text{dist}(x, y) = \varepsilon$.

Metric.ne_of_mem_sphere theorem

(h : y ∈ sphere x ε) (hε : ε ≠ 0) : y ≠ x

Full source

theorem ne_of_mem_sphere (h : y ∈ sphere x ε) (hε : ε ≠ 0) : y ≠ x :=
  ne_of_mem_of_not_mem h <| by simpa using hε.symm

Non-identity of Points on Nonzero Radius Spheres in Pseudometric Spaces

Informal description

For any point $y$ in a pseudometric space $\alpha$, if $y$ belongs to the sphere centered at $x$ with radius $\varepsilon \neq 0$, then $y$ is distinct from $x$, i.e., $y \neq x$.

Metric.nonneg_of_mem_sphere theorem

(hy : y ∈ sphere x ε) : 0 ≤ ε

Full source

theorem nonneg_of_mem_sphere (hy : y ∈ sphere x ε) : 0 ≤ ε :=
  dist_nonneg.trans_eq hy

Nonnegativity of Sphere Radius in Pseudometric Spaces

Informal description

For any point $y$ in a pseudometric space $\alpha$, if $y$ belongs to the sphere centered at $x$ with radius $\varepsilon$, then $\varepsilon$ is nonnegative, i.e., $\varepsilon \geq 0$.

Metric.sphere_eq_empty_of_neg theorem

(hε : ε < 0) : sphere x ε = ∅

Full source

@[simp]
theorem sphere_eq_empty_of_neg (hε : ε < 0) : sphere x ε = ∅ :=
  Set.eq_empty_iff_forall_not_mem.mpr fun _y hy => (nonneg_of_mem_sphere hy).not_lt hε

Empty Sphere Property for Negative Radii in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any negative real number $\varepsilon < 0$, the sphere centered at $x$ with radius $\varepsilon$ is empty, i.e., $\text{sphere}(x, \varepsilon) = \emptyset$.

Metric.sphere_eq_empty_of_subsingleton theorem

[Subsingleton α] (hε : ε ≠ 0) : sphere x ε = ∅

Full source

theorem sphere_eq_empty_of_subsingleton [Subsingleton α] (hε : ε ≠ 0) : sphere x ε = ∅ :=
  Set.eq_empty_iff_forall_not_mem.mpr fun _ h => ne_of_mem_sphere h hε (Subsingleton.elim _ _)

Empty Sphere Property in Subsingleton Pseudometric Spaces for $\varepsilon \neq 0$

Informal description

In a pseudometric space $\alpha$ that is a subsingleton (i.e., all elements are equal) and for any nonzero real number $\varepsilon \neq 0$, the sphere centered at any point $x \in \alpha$ with radius $\varepsilon$ is empty.

Metric.sphere_isEmpty_of_subsingleton instance

[Subsingleton α] [NeZero ε] : IsEmpty (sphere x ε)

Full source

instance sphere_isEmpty_of_subsingleton [Subsingleton α] [NeZero ε] : IsEmpty (sphere x ε) := by
  rw [sphere_eq_empty_of_subsingleton (NeZero.ne ε)]; infer_instance

Empty Sphere Property in Subsingleton Pseudometric Spaces for $\varepsilon \neq 0$

Informal description

In a pseudometric space $\alpha$ that is a subsingleton (i.e., all elements are equal) and for any nonzero real number $\varepsilon$, the sphere centered at any point $x \in \alpha$ with radius $\varepsilon$ is empty.

Metric.closedBall_eq_singleton_of_subsingleton theorem

[Subsingleton α] (h : 0 ≤ ε) : closedBall x ε = { x }

Full source

theorem closedBall_eq_singleton_of_subsingleton [Subsingleton α] (h : 0 ≤ ε) :
    closedBall x ε = {x} := by
  ext x'
  simpa [Subsingleton.allEq x x']

Closed Ball in Subsingleton Pseudometric Space is Singleton: $\overline{B}(x, \varepsilon) = \{x\}$ for $\varepsilon \geq 0$

Informal description

In a pseudometric space $\alpha$ that is a subsingleton (i.e., all elements are equal) and for any non-negative real number $\varepsilon \geq 0$, the closed ball centered at any point $x \in \alpha$ with radius $\varepsilon$ is equal to the singleton set $\{x\}$.

Metric.ball_eq_singleton_of_subsingleton theorem

[Subsingleton α] (h : 0 < ε) : ball x ε = { x }

Full source

theorem ball_eq_singleton_of_subsingleton [Subsingleton α] (h : 0 < ε) : ball x ε = {x} := by
  ext x'
  simpa [Subsingleton.allEq x x']

Open Ball in Subsingleton Pseudometric Space is Singleton: $B(x, \varepsilon) = \{x\}$ for $\varepsilon > 0$

Informal description

In a pseudometric space $\alpha$ that is a subsingleton (i.e., all elements are equal) and for any positive real number $\varepsilon > 0$, the open ball centered at any point $x \in \alpha$ with radius $\varepsilon$ is equal to the singleton set $\{x\}$.

Metric.mem_closedBall_self theorem

(h : 0 ≤ ε) : x ∈ closedBall x ε

Full source

theorem mem_closedBall_self (h : 0 ≤ ε) : x ∈ closedBall x ε := by
  rwa [mem_closedBall, dist_self]

Self-Membership in Closed Balls: $x \in \overline{B}(x, \varepsilon)$ for $\varepsilon \geq 0$

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon \geq 0$, the point $x$ belongs to the closed ball $\overline{B}(x, \varepsilon)$, i.e., $x \in \overline{B}(x, \varepsilon)$.

Metric.nonempty_closedBall theorem

: (closedBall x ε).Nonempty ↔ 0 ≤ ε

Full source

@[simp]
theorem nonempty_closedBall : (closedBall x ε).Nonempty ↔ 0 ≤ ε :=
  ⟨fun ⟨_x, hx⟩ => dist_nonneg.trans hx, fun h => ⟨x, mem_closedBall_self h⟩⟩

Nonemptiness of Closed Ball $\overline{B}(x, \varepsilon)$ iff $\varepsilon \geq 0$

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $\varepsilon$, the closed ball $\overline{B}(x, \varepsilon)$ is nonempty if and only if $\varepsilon \geq 0$.

Metric.closedBall_eq_empty theorem

: closedBall x ε = ∅ ↔ ε < 0

Full source

@[simp]
theorem closedBall_eq_empty : closedBallclosedBall x ε = ∅ ↔ ε < 0 := by
  rw [← not_nonempty_iff_eq_empty, nonempty_closedBall, not_le]

Empty Closed Ball Condition: $\overline{B}(x, \varepsilon) = \emptyset \leftrightarrow \varepsilon < 0$

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $\varepsilon$, the closed ball $\overline{B}(x, \varepsilon)$ is empty if and only if $\varepsilon < 0$.

Metric.closedBall_eq_sphere_of_nonpos theorem

(hε : ε ≤ 0) : closedBall x ε = sphere x ε

Full source

/-- Closed balls and spheres coincide when the radius is non-positive -/
theorem closedBall_eq_sphere_of_nonpos (hε : ε ≤ 0) : closedBall x ε = sphere x ε :=
  Set.ext fun _ => (hε.trans dist_nonneg).le_iff_eq

Closed Ball Equals Sphere for Non-Positive Radii

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-positive real number $\varepsilon \leq 0$, the closed ball $\overline{B}(x, \varepsilon)$ coincides with the sphere $S(x, \varepsilon)$. That is, $\overline{B}(x, \varepsilon) = \{ y \in \alpha \mid \text{dist}(y, x) \leq \varepsilon \} = \{ y \in \alpha \mid \text{dist}(y, x) = \varepsilon \} = S(x, \varepsilon)$.

Metric.ball_subset_closedBall theorem

: ball x ε ⊆ closedBall x ε

Full source

theorem ball_subset_closedBall : ballball x ε ⊆ closedBall x ε := fun _y hy =>
  mem_closedBall.2 (le_of_lt hy)

Open Ball is Subset of Closed Ball

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $\varepsilon > 0$, the open ball $B(x, \varepsilon)$ is contained in the closed ball $\overline{B}(x, \varepsilon)$. That is, $B(x, \varepsilon) \subseteq \overline{B}(x, \varepsilon)$.

Metric.sphere_subset_closedBall theorem

: sphere x ε ⊆ closedBall x ε

Full source

theorem sphere_subset_closedBall : spheresphere x ε ⊆ closedBall x ε := fun _ => le_of_eq

Sphere is Subset of Closed Ball in Pseudometric Space

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $\varepsilon \geq 0$, the sphere $S(x, \varepsilon)$ is contained in the closed ball $\overline{B}(x, \varepsilon)$. That is, $\{ y \in \alpha \mid \text{dist}(y, x) = \varepsilon \} \subseteq \{ y \in \alpha \mid \text{dist}(y, x) \leq \varepsilon \}$.

Metric.sphere_subset_ball theorem

{r R : ℝ} (h : r < R) : sphere x r ⊆ ball x R

Full source

lemma sphere_subset_ball {r R : ℝ} (h : r < R) : spheresphere x r ⊆ ball x R := fun _x hx ↦
  (mem_sphere.1 hx).trans_lt h

Sphere is Subset of Larger Ball in Pseudometric Space

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real numbers $r, R$ with $r < R$, the sphere centered at $x$ with radius $r$ is contained in the open ball centered at $x$ with radius $R$, i.e., $\text{sphere}(x, r) \subseteq \text{ball}(x, R)$.

Metric.closedBall_disjoint_ball theorem

(h : δ + ε ≤ dist x y) : Disjoint (closedBall x δ) (ball y ε)

Full source

theorem closedBall_disjoint_ball (h : δ + ε ≤ dist x y) : Disjoint (closedBall x δ) (ball y ε) :=
  Set.disjoint_left.mpr fun _a ha1 ha2 =>
    (h.trans <| dist_triangle_left _ _ _).not_lt <| add_lt_add_of_le_of_lt ha1 ha2

Disjointness of Closed and Open Balls under Sum Condition: $\delta + \varepsilon \leq \text{dist}(x, y)$

Informal description

For any points $x$ and $y$ in a pseudometric space $\alpha$ and any non-negative real numbers $\delta$ and $\varepsilon$ such that $\delta + \varepsilon \leq \text{dist}(x, y)$, the closed ball $\overline{B}(x, \delta)$ and the open ball $B(y, \varepsilon)$ are disjoint. That is, $\overline{B}(x, \delta) \cap B(y, \varepsilon) = \emptyset$.

Metric.ball_disjoint_closedBall theorem

(h : δ + ε ≤ dist x y) : Disjoint (ball x δ) (closedBall y ε)

Full source

theorem ball_disjoint_closedBall (h : δ + ε ≤ dist x y) : Disjoint (ball x δ) (closedBall y ε) :=
  (closedBall_disjoint_ball <| by rwa [add_comm, dist_comm]).symm

Disjointness of Open and Closed Balls under Sum Condition: $\delta + \varepsilon \leq \text{dist}(x, y)$

Informal description

For any points $x$ and $y$ in a pseudometric space $\alpha$ and any non-negative real numbers $\delta$ and $\varepsilon$ such that $\delta + \varepsilon \leq \text{dist}(x, y)$, the open ball $B(x, \delta)$ and the closed ball $\overline{B}(y, \varepsilon)$ are disjoint. That is, $B(x, \delta) \cap \overline{B}(y, \varepsilon) = \emptyset$.

Metric.ball_disjoint_ball theorem

(h : δ + ε ≤ dist x y) : Disjoint (ball x δ) (ball y ε)

Full source

theorem ball_disjoint_ball (h : δ + ε ≤ dist x y) : Disjoint (ball x δ) (ball y ε) :=
  (closedBall_disjoint_ball h).mono_left ball_subset_closedBall

Disjointness of Open Balls under Sum Condition: $\delta + \varepsilon \leq \text{dist}(x, y)$

Informal description

For any points $x$ and $y$ in a pseudometric space $\alpha$ and any non-negative real numbers $\delta$ and $\varepsilon$ such that $\delta + \varepsilon \leq \text{dist}(x, y)$, the open balls $B(x, \delta)$ and $B(y, \varepsilon)$ are disjoint. That is, $B(x, \delta) \cap B(y, \varepsilon) = \emptyset$.

Metric.closedBall_disjoint_closedBall theorem

(h : δ + ε < dist x y) : Disjoint (closedBall x δ) (closedBall y ε)

Full source

theorem closedBall_disjoint_closedBall (h : δ + ε < dist x y) :
    Disjoint (closedBall x δ) (closedBall y ε) :=
  Set.disjoint_left.mpr fun _a ha1 ha2 =>
    h.not_le <| (dist_triangle_left _ _ _).trans <| add_le_add ha1 ha2

Disjointness of Closed Balls in Pseudometric Spaces: $\delta + \varepsilon < \text{dist}(x, y) \Rightarrow \overline{B}(x, \delta) \cap \overline{B}(y, \varepsilon) = \emptyset$

Informal description

For any points $x$ and $y$ in a pseudometric space $\alpha$ and non-negative real numbers $\delta$ and $\varepsilon$, if $\delta + \varepsilon < \text{dist}(x, y)$, then the closed balls $\overline{B}(x, \delta)$ and $\overline{B}(y, \varepsilon)$ are disjoint.

Metric.sphere_disjoint_ball theorem

: Disjoint (sphere x ε) (ball x ε)

Full source

theorem sphere_disjoint_ball : Disjoint (sphere x ε) (ball x ε) :=
  Set.disjoint_left.mpr fun _y hy₁ hy₂ => absurd hy₁ <| ne_of_lt hy₂

Sphere and Open Ball are Disjoint in a Pseudometric Space

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the sphere $\{y \mid \text{dist}(y, x) = \varepsilon\}$ and the open ball $\{y \mid \text{dist}(y, x) < \varepsilon\}$ are disjoint sets.

Metric.ball_union_sphere theorem

: ball x ε ∪ sphere x ε = closedBall x ε

Full source

@[simp]
theorem ball_union_sphere : ballball x ε ∪ sphere x ε = closedBall x ε :=
  Set.ext fun _y => (@le_iff_lt_or_eq ℝ _ _ _).symm

Union of Open Ball and Sphere Equals Closed Ball

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the union of the open ball $\text{ball}(x, \varepsilon)$ and the sphere $\text{sphere}(x, \varepsilon)$ equals the closed ball $\overline{B}(x, \varepsilon)$. That is, \[ \text{ball}(x, \varepsilon) \cup \text{sphere}(x, \varepsilon) = \overline{B}(x, \varepsilon). \]

Metric.sphere_union_ball theorem

: sphere x ε ∪ ball x ε = closedBall x ε

Full source

@[simp]
theorem sphere_union_ball : spheresphere x ε ∪ ball x ε = closedBall x ε := by
  rw [union_comm, ball_union_sphere]

Union of Sphere and Open Ball Equals Closed Ball

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the union of the sphere $\text{sphere}(x, \varepsilon)$ and the open ball $\text{ball}(x, \varepsilon)$ equals the closed ball $\overline{B}(x, \varepsilon)$. That is, \[ \text{sphere}(x, \varepsilon) \cup \text{ball}(x, \varepsilon) = \overline{B}(x, \varepsilon). \]

Metric.closedBall_diff_sphere theorem

: closedBall x ε \ sphere x ε = ball x ε

Full source

@[simp]
theorem closedBall_diff_sphere : closedBallclosedBall x ε \ sphere x ε = ball x ε := by
  rw [← ball_union_sphere, Set.union_diff_cancel_right sphere_disjoint_ball.symm.le_bot]

Closed Ball Minus Sphere Equals Open Ball: $\overline{B}(x, \varepsilon) \setminus \text{sphere}(x, \varepsilon) = \text{ball}(x, \varepsilon)$

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the set difference between the closed ball $\overline{B}(x, \varepsilon)$ and the sphere $\{y \mid \text{dist}(y, x) = \varepsilon\}$ equals the open ball $\{y \mid \text{dist}(y, x) < \varepsilon\}$. That is, \[ \overline{B}(x, \varepsilon) \setminus \{y \mid \text{dist}(y, x) = \varepsilon\} = \{y \mid \text{dist}(y, x) < \varepsilon\}. \]

Metric.closedBall_diff_ball theorem

: closedBall x ε \ ball x ε = sphere x ε

Full source

@[simp]
theorem closedBall_diff_ball : closedBallclosedBall x ε \ ball x ε = sphere x ε := by
  rw [← ball_union_sphere, Set.union_diff_cancel_left sphere_disjoint_ball.symm.le_bot]

Closed Ball Minus Open Ball Equals Sphere: $\overline{B}(x, \varepsilon) \setminus B(x, \varepsilon) = \{y \mid \text{dist}(y, x) = \varepsilon\}$

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the set difference between the closed ball $\overline{B}(x, \varepsilon)$ and the open ball $B(x, \varepsilon)$ equals the sphere $\{y \mid \text{dist}(y, x) = \varepsilon\}$. That is, \[ \overline{B}(x, \varepsilon) \setminus B(x, \varepsilon) = \{y \mid \text{dist}(y, x) = \varepsilon\}. \]

Metric.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 Open Ball Membership: $x \in B(y, \varepsilon) \leftrightarrow y \in B(x, \varepsilon)$

Informal description

For any points $x$ and $y$ in a pseudometric space and any positive real number $\varepsilon$, 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$, i.e., $x \in \text{ball}(y, \varepsilon) \leftrightarrow y \in \text{ball}(x, \varepsilon)$.

Metric.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]

Symmetric Property of Closed Ball Membership in Pseudometric Spaces

Informal description

For any points $x$ and $y$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, 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 \overline{B}(y, \varepsilon) \leftrightarrow y \in \overline{B}(x, \varepsilon)$.

Metric.mem_sphere_comm theorem

: x ∈ sphere y ε ↔ y ∈ sphere x ε

Full source

theorem mem_sphere_comm : x ∈ sphere y εx ∈ sphere y ε ↔ y ∈ sphere x ε := by rw [mem_sphere', mem_sphere]

Symmetry of Sphere Membership: $x \in S(y, \varepsilon) \leftrightarrow y \in S(x, \varepsilon)$

Informal description

For any points $x$ and $y$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the point $x$ belongs to the sphere centered at $y$ with radius $\varepsilon$ if and only if $y$ belongs to the sphere centered at $x$ with radius $\varepsilon$, i.e., $$x \in \text{sphere}(y, \varepsilon) \leftrightarrow y \in \text{sphere}(x, \varepsilon).$$

Metric.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 (mem_ball.1 yx) h

Monotonicity of Open Balls: $B(x, \varepsilon_1) \subseteq B(x, \varepsilon_2)$ for $\varepsilon_1 \leq \varepsilon_2$

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any two non-negative real numbers $\varepsilon_1$ and $\varepsilon_2$ such that $\varepsilon_1 \leq \varepsilon_2$, the open ball centered at $x$ with radius $\varepsilon_1$ is a subset of the open ball centered at $x$ with radius $\varepsilon_2$, i.e., $$B(x, \varepsilon_1) \subseteq B(x, \varepsilon_2).$$

Metric.closedBall_eq_bInter_ball theorem

: closedBall x ε = ⋂ δ > ε, ball x δ

Full source

theorem closedBall_eq_bInter_ball : closedBall x ε = ⋂ δ > ε, ball x δ := by
  ext y; rw [mem_closedBall, ← forall_lt_iff_le', mem_iInter₂]; rfl

Closed Ball as Intersection of Open Balls: $\overline{B}(x, \varepsilon) = \bigcap_{\delta > \varepsilon} B(x, \delta)$

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the closed ball $\overline{B}(x, \varepsilon)$ centered at $x$ with radius $\varepsilon$ is equal to the intersection of all open balls $B(x, \delta)$ with radius $\delta > \varepsilon$, i.e., $$\overline{B}(x, \varepsilon) = \bigcap_{\delta > \varepsilon} B(x, \delta).$$

Metric.ball_subset_ball' theorem

(h : ε₁ + dist x y ≤ ε₂) : ball x ε₁ ⊆ ball y ε₂

Full source

theorem ball_subset_ball' (h : ε₁ + dist x y ≤ ε₂) : ballball x ε₁ ⊆ ball y ε₂ := fun z hz =>
  calc
    dist z y ≤ dist z x + dist x y := dist_triangle _ _ _
    _ < ε₁ + dist x y := add_lt_add_right (mem_ball.1 hz) _
    _ ≤ ε₂ := h

Open Ball Inclusion via Distance Sum: $B(x, \varepsilon_1) \subseteq B(y, \varepsilon_2)$ when $\varepsilon_1 + d(x,y) \leq \varepsilon_2$

Informal description

For any points $x, y$ in a pseudometric space $\alpha$ and any non-negative real numbers $\varepsilon_1, \varepsilon_2$, if $\varepsilon_1 + \text{dist}(x, y) \leq \varepsilon_2$, then the open ball centered at $x$ with radius $\varepsilon_1$ is contained in the open ball centered at $y$ with radius $\varepsilon_2$, i.e., $$B(x, \varepsilon_1) \subseteq B(y, \varepsilon_2).$$

Metric.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 with Respect to Radius

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real numbers $\varepsilon_1$ and $\varepsilon_2$ such that $\varepsilon_1 \leq \varepsilon_2$, the closed ball $\overline{B}(x, \varepsilon_1)$ is a subset of the closed ball $\overline{B}(x, \varepsilon_2)$, i.e., $$\overline{B}(x, \varepsilon_1) \subseteq \overline{B}(x, \varepsilon_2).$$

Metric.closedBall_subset_closedBall' theorem

(h : ε₁ + dist x y ≤ ε₂) : closedBall x ε₁ ⊆ closedBall y ε₂

Full source

theorem closedBall_subset_closedBall' (h : ε₁ + dist x y ≤ ε₂) :
    closedBallclosedBall x ε₁ ⊆ closedBall y ε₂ := fun z hz =>
  calc
    dist z y ≤ dist z x + dist x y := dist_triangle _ _ _
    _ ≤ ε₁ + dist x y := add_le_add_right (mem_closedBall.1 hz) _
    _ ≤ ε₂ := h

Inclusion of Closed Balls under Distance Condition: $\overline{B}(x, \varepsilon_1) \subseteq \overline{B}(y, \varepsilon_2)$ when $\varepsilon_1 + d(x,y) \leq \varepsilon_2$

Informal description

For any points $x, y$ in a pseudometric space $\alpha$ and non-negative real numbers $\varepsilon_1, \varepsilon_2$, if $\varepsilon_1 + \text{dist}(x, y) \leq \varepsilon_2$, then the closed ball $\overline{B}(x, \varepsilon_1)$ is contained in the closed ball $\overline{B}(y, \varepsilon_2)$.

Metric.closedBall_subset_ball theorem

(h : ε₁ < ε₂) : closedBall x ε₁ ⊆ ball x ε₂

Full source

theorem closedBall_subset_ball (h : ε₁ < ε₂) : closedBallclosedBall x ε₁ ⊆ ball x ε₂ :=
  fun y (yh : dist y x ≤ ε₁) => lt_of_le_of_lt yh h

Closed Ball is Subset of Larger Open Ball

Informal description

For any point $x$ in a pseudometric space $\alpha$ and real numbers $\varepsilon_1, \varepsilon_2$ with $\varepsilon_1 < \varepsilon_2$, the closed ball $\overline{B}(x, \varepsilon_1)$ is contained in the open ball $B(x, \varepsilon_2)$.

Metric.closedBall_subset_ball' theorem

(h : ε₁ + dist x y < ε₂) : closedBall x ε₁ ⊆ ball y ε₂

Full source

theorem closedBall_subset_ball' (h : ε₁ + dist x y < ε₂) :
    closedBallclosedBall x ε₁ ⊆ ball y ε₂ := fun z hz =>
  calc
    dist z y ≤ dist z x + dist x y := dist_triangle _ _ _
    _ ≤ ε₁ + dist x y := add_le_add_right (mem_closedBall.1 hz) _
    _ < ε₂ := h

Inclusion of Closed Ball in Open Ball via Distance Sum Condition

Informal description

For any points $x, y$ in a pseudometric space $\alpha$ and non-negative real numbers $\varepsilon_1, \varepsilon_2$, if $\varepsilon_1 + \text{dist}(x, y) < \varepsilon_2$, then the closed ball $\overline{B}(x, \varepsilon_1)$ is contained in the open ball $B(y, \varepsilon_2)$.

Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall theorem

(h : (closedBall x ε₁ ∩ closedBall y ε₂).Nonempty) : dist x y ≤ ε₁ + ε₂

Full source

theorem dist_le_add_of_nonempty_closedBall_inter_closedBall
    (h : (closedBallclosedBall x ε₁ ∩ closedBall y ε₂).Nonempty) : dist x y ≤ ε₁ + ε₂ :=
  let ⟨z, hz⟩ := h
  calc
    dist x y ≤ dist z x + dist z y := dist_triangle_left _ _ _
    _ ≤ ε₁ + ε₂ := add_le_add hz.1 hz.2

Distance Bound from Nonempty Intersection of Closed Balls

Informal description

For any two points $x$ and $y$ in a pseudometric space $\alpha$, and any non-negative real numbers $\varepsilon_1$ and $\varepsilon_2$, if the intersection of the closed balls $\overline{B}(x, \varepsilon_1)$ and $\overline{B}(y, \varepsilon_2)$ is nonempty, then the distance between $x$ and $y$ satisfies $d(x, y) \leq \varepsilon_1 + \varepsilon_2$.

Metric.dist_lt_add_of_nonempty_closedBall_inter_ball theorem

(h : (closedBall x ε₁ ∩ ball y ε₂).Nonempty) : dist x y < ε₁ + ε₂

Full source

theorem dist_lt_add_of_nonempty_closedBall_inter_ball (h : (closedBallclosedBall x ε₁ ∩ ball y ε₂).Nonempty) :
    dist x y < ε₁ + ε₂ :=
  let ⟨z, hz⟩ := h
  calc
    dist x y ≤ dist z x + dist z y := dist_triangle_left _ _ _
    _ < ε₁ + ε₂ := add_lt_add_of_le_of_lt hz.1 hz.2

Distance Bound from Nonempty Intersection of Closed and Open Balls

Informal description

For any points $x, y$ in a pseudometric space $\alpha$ and non-negative real numbers $\varepsilon_1, \varepsilon_2$, if the intersection of the closed ball $\overline{B}(x, \varepsilon_1)$ and the open ball $B(y, \varepsilon_2)$ is nonempty, then the distance between $x$ and $y$ satisfies $d(x, y) < \varepsilon_1 + \varepsilon_2$.

Metric.dist_lt_add_of_nonempty_ball_inter_closedBall theorem

(h : (ball x ε₁ ∩ closedBall y ε₂).Nonempty) : dist x y < ε₁ + ε₂

Full source

theorem dist_lt_add_of_nonempty_ball_inter_closedBall (h : (ballball x ε₁ ∩ closedBall y ε₂).Nonempty) :
    dist x y < ε₁ + ε₂ := by
  rw [inter_comm] at h
  rw [add_comm, dist_comm]
  exact dist_lt_add_of_nonempty_closedBall_inter_ball h

Distance Bound from Nonempty Intersection of Open and Closed Balls: $d(x,y) < \varepsilon_1 + \varepsilon_2$

Informal description

For any points $x, y$ in a pseudometric space $\alpha$ and non-negative real numbers $\varepsilon_1, \varepsilon_2$, if the intersection of the open ball $B(x, \varepsilon_1)$ and the closed ball $\overline{B}(y, \varepsilon_2)$ is nonempty, then the distance between $x$ and $y$ satisfies $d(x, y) < \varepsilon_1 + \varepsilon_2$.

Metric.dist_lt_add_of_nonempty_ball_inter_ball theorem

(h : (ball x ε₁ ∩ ball y ε₂).Nonempty) : dist x y < ε₁ + ε₂

Full source

theorem dist_lt_add_of_nonempty_ball_inter_ball (h : (ballball x ε₁ ∩ ball y ε₂).Nonempty) :
    dist x y < ε₁ + ε₂ :=
  dist_lt_add_of_nonempty_closedBall_inter_ball <|
    h.mono (inter_subset_inter ball_subset_closedBall Subset.rfl)

Distance Bound from Nonempty Intersection of Open Balls: $d(x,y) < \varepsilon_1 + \varepsilon_2$

Informal description

For any points $x, y$ in a pseudometric space $\alpha$ and non-negative real numbers $\varepsilon_1, \varepsilon_2$, if the intersection of the open balls $B(x, \varepsilon_1)$ and $B(y, \varepsilon_2)$ is nonempty, then the distance between $x$ and $y$ satisfies $d(x, y) < \varepsilon_1 + \varepsilon_2$.

Metric.iUnion_closedBall_nat theorem

(x : α) : ⋃ n : ℕ, closedBall x n = univ

Full source

@[simp]
theorem iUnion_closedBall_nat (x : α) : ⋃ n : ℕ, closedBall x n = univ :=
  iUnion_eq_univ_iff.2 fun y => exists_nat_ge (dist y x)

Union of Closed Balls Covers the Space

Informal description

For any point $x$ in a pseudometric space $\alpha$, the union of closed balls centered at $x$ with radii ranging over all natural numbers equals the entire space. That is, \[ \bigcup_{n \in \mathbb{N}} \overline{B}(x, n) = \alpha. \]

Metric.iUnion_inter_closedBall_nat theorem

(s : Set α) (x : α) : ⋃ n : ℕ, s ∩ closedBall x n = s

Full source

theorem iUnion_inter_closedBall_nat (s : Set α) (x : α) : ⋃ n : ℕ, s ∩ closedBall x n = s := by
  rw [← inter_iUnion, iUnion_closedBall_nat, inter_univ]

Union of Intersections with Closed Balls Equals Original Set

Informal description

For any subset $s$ of a pseudometric space $\alpha$ and any point $x \in \alpha$, the union of the intersections of $s$ with closed balls centered at $x$ of radius $n$ over all natural numbers $n$ equals $s$. That is, \[ \bigcup_{n \in \mathbb{N}} (s \cap \overline{B}(x, n)) = s. \]

Metric.ball_subset theorem

(h : dist x y ≤ ε₂ - ε₁) : ball x ε₁ ⊆ ball y ε₂

Full source

theorem ball_subset (h : dist x y ≤ ε₂ - ε₁) : ballball x ε₁ ⊆ ball y ε₂ := fun z zx => by
  rw [← add_sub_cancel ε₁ ε₂]
  exact lt_of_le_of_lt (dist_triangle z x y) (add_lt_add_of_lt_of_le zx h)

Inclusion of Open Balls in Pseudometric Spaces: $B(x, \varepsilon_1) \subseteq B(y, \varepsilon_2)$ when $\text{dist}(x, y) \leq \varepsilon_2 - \varepsilon_1$

Informal description

Let $\alpha$ be a pseudometric space with distance function $\text{dist}$. For any points $x, y \in \alpha$ and real numbers $\varepsilon_1, \varepsilon_2 > 0$, if $\text{dist}(x, y) \leq \varepsilon_2 - \varepsilon_1$, then the open ball centered at $x$ with radius $\varepsilon_1$ is contained in the open ball centered at $y$ with radius $\varepsilon_2$, i.e., \[ B(x, \varepsilon_1) \subseteq B(y, \varepsilon_2). \]

Metric.ball_half_subset theorem

(y) (h : y ∈ ball x (ε / 2)) : ball y (ε / 2) ⊆ ball x ε

Full source

theorem ball_half_subset (y) (h : y ∈ ball x (ε / 2)) : ballball y (ε / 2) ⊆ ball x ε :=
  ball_subset <| by rw [sub_self_div_two]; exact le_of_lt h

Half-Radius Ball Inclusion in Pseudometric Spaces: $B(y, \varepsilon/2) \subseteq B(x, \varepsilon)$ when $y \in B(x, \varepsilon/2)$

Informal description

Let $\alpha$ be a pseudometric space with distance function $\text{dist}$. For any point $x \in \alpha$, radius $\varepsilon > 0$, and point $y \in B(x, \varepsilon/2)$, the open ball centered at $y$ with radius $\varepsilon/2$ is contained in the open ball centered at $x$ with radius $\varepsilon$, i.e., \[ B(y, \varepsilon/2) \subseteq B(x, \varepsilon). \]

Metric.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 ε :=
  ⟨_, sub_pos.2 h, ball_subset <| by rw [sub_sub_self]⟩

Existence of Nested Open Balls in Pseudometric Spaces: $B(y, \varepsilon') \subseteq B(x, \varepsilon)$ when $y \in B(x, \varepsilon)$

Informal description

Let $\alpha$ be a pseudometric space with distance function $\text{dist}$. For any points $x, y \in \alpha$ and $\varepsilon > 0$, if $y$ belongs to the open ball $B(x, \varepsilon)$, then there exists $\varepsilon' > 0$ such that the open ball $B(y, \varepsilon')$ is contained in $B(x, \varepsilon)$.

Metric.forall_of_forall_mem_closedBall theorem

(p : α → Prop) (x : α) (H : ∃ᶠ R : ℝ in atTop, ∀ y ∈ closedBall x R, p y) (y : α) : p y

Full source

/-- If a property holds for all points in closed balls of arbitrarily large radii, then it holds for
all points. -/
theorem forall_of_forall_mem_closedBall (p : α → Prop) (x : α)
    (H : ∃ᶠ R : ℝ in atTop, ∀ y ∈ closedBall x R, p y) (y : α) : p y := by
  obtain ⟨R, hR, h⟩ : ∃ R ≥ dist y x, ∀ z : α, z ∈ closedBall x R → p z :=
    frequently_iff.1 H (Ici_mem_atTop (dist y x))
  exact h _ hR

Global Property from Large Closed Balls in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $p : \alpha \to \mathrm{Prop}$ a property on $\alpha$, and $x \in \alpha$. If for arbitrarily large radii $R$, the property $p$ holds for all points in the closed ball $\overline{B}(x, R)$, then $p$ holds for all points $y \in \alpha$.

Metric.forall_of_forall_mem_ball theorem

(p : α → Prop) (x : α) (H : ∃ᶠ R : ℝ in atTop, ∀ y ∈ ball x R, p y) (y : α) : p y

Full source

/-- If a property holds for all points in balls of arbitrarily large radii, then it holds for all
points. -/
theorem forall_of_forall_mem_ball (p : α → Prop) (x : α)
    (H : ∃ᶠ R : ℝ in atTop, ∀ y ∈ ball x R, p y) (y : α) : p y := by
  obtain ⟨R, hR, h⟩ : ∃ R > dist y x, ∀ z : α, z ∈ ball x R → p z :=
    frequently_iff.1 H (Ioi_mem_atTop (dist y x))
  exact h _ hR

Global Property from Large Open Balls in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $p : \alpha \to \mathrm{Prop}$ a property on $\alpha$, and $x \in \alpha$. If for arbitrarily large radii $R$, the property $p$ holds for all points in the open ball $B(x, R)$, then $p$ holds for all points $y \in \alpha$.

Metric.isBounded_iff theorem

{s : Set α} : IsBounded s ↔ ∃ C : ℝ, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C

Full source

theorem isBounded_iff {s : Set α} :
    IsBoundedIsBounded s ↔ ∃ C : ℝ, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C := by
  rw [isBounded_def, ← Filter.mem_sets, @PseudoMetricSpace.cobounded_sets α, mem_setOf_eq,
    compl_compl]

Characterization of Bounded Sets in Pseudometric Spaces

Informal description

A subset $s$ of a pseudometric space $\alpha$ is bounded if and only if there exists a real number $C$ such that for all $x, y \in s$, the distance between $x$ and $y$ satisfies $\text{dist}(x, y) \leq C$.

Metric.isBounded_iff_eventually theorem

{s : Set α} : IsBounded s ↔ ∀ᶠ C in atTop, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C

Full source

theorem isBounded_iff_eventually {s : Set α} :
    IsBoundedIsBounded s ↔ ∀ᶠ C in atTop, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C :=
  isBounded_iff.trans
    ⟨fun ⟨C, h⟩ => eventually_atTop.2 ⟨C, fun _C' hC' _x hx _y hy => (h hx hy).trans hC'⟩,
      Eventually.exists⟩

Eventual Uniform Boundedness Characterization in Pseudometric Spaces

Informal description

A subset $s$ of a pseudometric space $\alpha$ is bounded if and only if for all sufficiently large real numbers $C$, the distance between any two points $x, y \in s$ satisfies $\text{dist}(x, y) \leq C$.

Metric.isBounded_iff_exists_ge theorem

 {s : Set α} (c : ℝ) : IsBounded s ↔ ∃ C, c ≤ C ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C

Full source

theorem isBounded_iff_exists_ge {s : Set α} (c : ℝ) :
    IsBoundedIsBounded s ↔ ∃ C, c ≤ C ∧ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → dist x y ≤ C :=
  ⟨fun h => ((eventually_ge_atTop c).and (isBounded_iff_eventually.1 h)).exists, fun h =>
    isBounded_iff.2 <| h.imp fun _ => And.right⟩

Boundedness Criterion with Lower Bound in Pseudometric Spaces

Informal description

For any subset $s$ of a pseudometric space $\alpha$ and any real number $c$, the set $s$ is bounded if and only if there exists a real number $C \geq c$ such that for all $x, y \in s$, the distance satisfies $\text{dist}(x, y) \leq C$.

Metric.isBounded_iff_nndist theorem

{s : Set α} : IsBounded s ↔ ∃ C : ℝ≥0, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → nndist x y ≤ C

Full source

theorem isBounded_iff_nndist {s : Set α} :
    IsBoundedIsBounded s ↔ ∃ C : ℝ≥0, ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → nndist x y ≤ C := by
  simp only [isBounded_iff_exists_ge 0, NNReal.exists, ← NNReal.coe_le_coe, ← dist_nndist,
    NNReal.coe_mk, exists_prop]

Boundedness Criterion via Non-negative Distance in Pseudometric Spaces

Informal description

A subset $s$ of a pseudometric space $\alpha$ is bounded if and only if there exists a non-negative real number $C$ such that for all $x, y \in s$, the non-negative distance $\text{nndist}(x, y) \leq C$.

Metric.toUniformSpace_eq theorem

: ‹PseudoMetricSpace α›.toUniformSpace = .ofDist dist dist_self dist_comm dist_triangle

Full source

theorem toUniformSpace_eq :
    ‹PseudoMetricSpace α›.toUniformSpace = .ofDist dist dist_self dist_comm dist_triangle :=
  UniformSpace.ext PseudoMetricSpace.uniformity_dist

Equality of Pseudometric-Induced Uniform Space and Distance-Constructed Uniform Space

Informal description

For any pseudometric space $\alpha$ with distance function $\text{dist}$, the uniform space structure induced by the pseudometric is equal to the uniform space constructed from $\text{dist}$ using the reflexivity, symmetry, and triangle inequality properties.

Metric.uniformity_basis_dist theorem

: (𝓤 α).HasBasis (fun ε : ℝ => 0 < ε) fun ε => {p : α × α | dist p.1 p.2 < ε}

Full source

theorem uniformity_basis_dist :
    (𝓤 α).HasBasis (fun ε : ℝ => 0 < ε) fun ε => { p : α × α | dist p.1 p.2 < ε } := by
  rw [toUniformSpace_eq]
  exact UniformSpace.hasBasis_ofFun (exists_gt _) _ _ _ _ _

Basis for Uniformity Filter via Distance in Pseudometric Spaces

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudometric space $\alpha$ has a basis consisting of the sets $\{(x, y) \mid \text{dist}(x, y) < \varepsilon\}$ for all positive real numbers $\varepsilon > 0$.

Metric.mk_uniformity_basis theorem

 {β : Type*} {p : β → Prop} {f : β → ℝ} (hf₀ : ∀ i, p i → 0 < f i) (hf : ∀ ⦃ε⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε) :
  (𝓤 α).HasBasis p fun i => {p : α × α | dist p.1 p.2 < f i}

Full source

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

For specific bases see `uniformity_basis_dist`, `uniformity_basis_dist_inv_nat_succ`,
and `uniformity_basis_dist_inv_nat_pos`. -/
protected theorem mk_uniformity_basis {β : Type*} {p : β → Prop} {f : β → ℝ}
    (hf₀ : ∀ i, p i → 0 < f i) (hf : ∀ ⦃ε⦄, 0 < ε → ∃ i, p i ∧ f i ≤ ε) :
    (𝓤 α).HasBasis p fun i => { p : α × α | dist p.1 p.2 < f i } := by
  refine ⟨fun s => uniformity_basis_dist.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 H⟩
  · exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, H⟩

Basis Construction for Uniformity Filter via Positive Real-Valued Function

Informal description

Let $\alpha$ be a pseudometric space, $\beta$ a type, $p : \beta \to \text{Prop}$ a predicate on $\beta$, and $f : \beta \to \mathbb{R}$ a function. Suppose that: 1. For every $i \in \beta$ satisfying $p(i)$, we have $f(i) > 0$. 2. For every $\varepsilon > 0$, there exists $i \in \beta$ such that $p(i)$ holds and $f(i) \leq \varepsilon$. Then the uniformity filter $\mathfrak{U}(\alpha)$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{dist}(x, y) < f(i)\}$ for all $i \in \beta$ satisfying $p(i)$.

Metric.uniformity_basis_dist_rat theorem

: (𝓤 α).HasBasis (fun r : ℚ => 0 < r) fun r => {p : α × α | dist p.1 p.2 < r}

Full source

theorem uniformity_basis_dist_rat :
    (𝓤 α).HasBasis (fun r : ℚ => 0 < r) fun r => { p : α × α | dist p.1 p.2 < r } :=
  Metric.mk_uniformity_basis (fun _ => Rat.cast_pos.2) fun _ε hε =>
    let ⟨r, hr0, hrε⟩ := exists_rat_btwn hε
    ⟨r, Rat.cast_pos.1 hr0, hrε.le⟩

Rational Distance Basis for Uniformity in Pseudometric Spaces

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudometric space $\alpha$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{dist}(x, y) < r\}$ for all positive rational numbers $r > 0$.

Metric.uniformity_basis_dist_inv_nat_succ theorem

: (𝓤 α).HasBasis (fun _ => True) fun n : ℕ => {p : α × α | dist p.1 p.2 < 1 / (↑n + 1)}

Full source

theorem uniformity_basis_dist_inv_nat_succ :
    (𝓤 α).HasBasis (fun _ => True) fun n : ℕ => { p : α × α | dist p.1 p.2 < 1 / (↑n + 1) } :=
  Metric.mk_uniformity_basis (fun n _ => div_pos zero_lt_one <| Nat.cast_add_one_pos n) fun _ε ε0 =>
    (exists_nat_one_div_lt ε0).imp fun _n hn => ⟨trivial, le_of_lt hn⟩

Uniformity Basis via Reciprocal of Successor Natural Numbers in Pseudometric Spaces

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudometric space $\alpha$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{dist}(x, y) < \frac{1}{n + 1}\}$ for all natural numbers $n \in \mathbb{N}$.

Metric.uniformity_basis_dist_inv_nat_pos theorem

: (𝓤 α).HasBasis (fun n : ℕ => 0 < n) fun n : ℕ => {p : α × α | dist p.1 p.2 < 1 / ↑n}

Full source

theorem uniformity_basis_dist_inv_nat_pos :
    (𝓤 α).HasBasis (fun n : ℕ => 0 < n) fun n : ℕ => { p : α × α | dist p.1 p.2 < 1 / ↑n } :=
  Metric.mk_uniformity_basis (fun _ hn => div_pos zero_lt_one <| Nat.cast_pos.2 hn) fun _ ε0 =>
    let ⟨n, hn⟩ := exists_nat_one_div_lt ε0
    ⟨n + 1, Nat.succ_pos n, mod_cast hn.le⟩

Basis for Uniformity Filter via Inverse Natural Numbers in Pseudometric Spaces

Informal description

For a pseudometric space $\alpha$, the uniformity filter $\mathfrak{U}(\alpha)$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{dist}(x, y) < \frac{1}{n}\}$ for all positive natural numbers $n \in \mathbb{N}$.

Metric.uniformity_basis_dist_pow theorem

 {r : ℝ} (h0 : 0 < r) (h1 : r < 1) : (𝓤 α).HasBasis (fun _ : ℕ => True) fun n : ℕ => {p : α × α | dist p.1 p.2 < r ^ n}

Full source

theorem uniformity_basis_dist_pow {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
    (𝓤 α).HasBasis (fun _ : ℕ => True) fun n : ℕ => { p : α × α | dist p.1 p.2 < r ^ n } :=
  Metric.mk_uniformity_basis (fun _ _ => pow_pos h0 _) fun _ε ε0 =>
    let ⟨n, hn⟩ := exists_pow_lt_of_lt_one ε0 h1
    ⟨n, trivial, hn.le⟩

Uniformity Basis via Powers of $r$ in Pseudometric Spaces for $0 < r < 1$

Informal description

Let $\alpha$ be a pseudometric space and let $r \in \mathbb{R}$ satisfy $0 < r < 1$. Then the uniformity filter $\mathfrak{U}(\alpha)$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{dist}(x, y) < r^n\}$ for all natural numbers $n \in \mathbb{N}$.

Metric.uniformity_basis_dist_lt theorem

{R : ℝ} (hR : 0 < R) : (𝓤 α).HasBasis (fun r : ℝ => 0 < r ∧ r < R) fun r => {p : α × α | dist p.1 p.2 < r}

Full source

theorem uniformity_basis_dist_lt {R : ℝ} (hR : 0 < R) :
    (𝓤 α).HasBasis (fun r : ℝ => 0 < r ∧ r < R) fun r => { p : α × α | dist p.1 p.2 < r } :=
  Metric.mk_uniformity_basis (fun _ => And.left) fun r hr =>
    ⟨min r (R / 2), ⟨lt_min hr (half_pos hR), min_lt_iff.2 <| Or.inr (half_lt_self hR)⟩,
      min_le_left _ _⟩

Uniformity Basis via Distance Balls in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $R$ a positive real number. The uniformity filter $\mathfrak{U}(\alpha)$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{dist}(x, y) < r\}$ for all real numbers $r$ satisfying $0 < r < R$.

Metric.mk_uniformity_basis_le theorem

 {β : Type*} {p : β → Prop} {f : β → ℝ} (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x, p x ∧ f x ≤ ε) :
  (𝓤 α).HasBasis p fun x => {p : α × α | dist p.1 p.2 ≤ f x}

Full source

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

Currently we have only one specific basis `uniformity_basis_dist_le` based on this constructor.
More can be easily added if needed in the future. -/
protected theorem mk_uniformity_basis_le {β : Type*} {p : β → Prop} {f : β → ℝ}
    (hf₀ : ∀ x, p x → 0 < f x) (hf : ∀ ε, 0 < ε → ∃ x, p x ∧ f x ≤ ε) :
    (𝓤 α).HasBasis p fun x => { p : α × α | dist p.1 p.2 ≤ f x } := by
  refine ⟨fun s => uniformity_basis_dist.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 H) hε'.2⟩
  · exact fun ⟨i, hi, H⟩ => ⟨f i, hf₀ i hi, fun x (hx : _ < _) => H (mem_setOf.2 hx.le)⟩

Basis Construction for Uniformity Filter via Distance Bounds in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $\beta$ a type, $p : \beta \to \text{Prop}$ a predicate on $\beta$, and $f : \beta \to \mathbb{R}$ a function. Suppose that: 1. For every $x \in \beta$ satisfying $p(x)$, the value $f(x)$ is positive. 2. For every $\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 $\{(x, y) \in \alpha \times \alpha \mid \text{dist}(x, y) \leq f(z)\}$ for all $z \in \beta$ satisfying $p(z)$.

Metric.uniformity_basis_dist_le theorem

: (𝓤 α).HasBasis ((0 : ℝ) < ·) fun ε => {p : α × α | dist p.1 p.2 ≤ ε}

Full source

/-- Constant size closed neighborhoods of the diagonal form a basis
of the uniformity filter. -/
theorem uniformity_basis_dist_le :
    (𝓤 α).HasBasis ((0 : ℝ) < ·) fun ε => { p : α × α | dist p.1 p.2 ≤ ε } :=
  Metric.mk_uniformity_basis_le (fun _ => id) fun ε ε₀ => ⟨ε, ε₀, le_refl ε⟩

Basis of Uniformity Filter via Closed Distance Balls in Pseudometric Spaces

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudometric space $\alpha$ has a basis consisting of all sets of pairs $(x, y) \in \alpha \times \alpha$ such that $\text{dist}(x, y) \leq \varepsilon$ for some $\varepsilon > 0$.

Metric.uniformity_basis_dist_le_pow theorem

 {r : ℝ} (h0 : 0 < r) (h1 : r < 1) : (𝓤 α).HasBasis (fun _ : ℕ => True) fun n : ℕ => {p : α × α | dist p.1 p.2 ≤ r ^ n}

Full source

theorem uniformity_basis_dist_le_pow {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
    (𝓤 α).HasBasis (fun _ : ℕ => True) fun n : ℕ => { p : α × α | dist p.1 p.2 ≤ r ^ n } :=
  Metric.mk_uniformity_basis_le (fun _ _ => pow_pos h0 _) fun _ε ε0 =>
    let ⟨n, hn⟩ := exists_pow_lt_of_lt_one ε0 h1
    ⟨n, trivial, hn.le⟩

Uniformity Basis via Geometric Distance Bounds in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $r \in \mathbb{R}$ such that $0 < r < 1$. Then the uniformity filter $\mathfrak{U}(\alpha)$ has a basis consisting of the sets $\{(x, y) \in \alpha \times \alpha \mid \text{dist}(x, y) \leq r^n\}$ for all natural numbers $n \in \mathbb{N}$.

Metric.mem_uniformity_dist theorem

{s : Set (α × α)} : s ∈ 𝓤 α ↔ ∃ ε > 0, ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ s

Full source

theorem mem_uniformity_dist {s : Set (α × α)} :
    s ∈ 𝓤 αs ∈ 𝓤 α ↔ ∃ ε > 0, ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ s :=
  uniformity_basis_dist.mem_uniformity_iff

Characterization of Uniformity Membership via Distance in Pseudometric Spaces

Informal description

For any set $s \subseteq \alpha \times \alpha$ in a pseudometric 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 $\text{dist}(a, b) < \varepsilon$ then $(a, b) \in s$.

Metric.dist_mem_uniformity theorem

{ε : ℝ} (ε0 : 0 < ε) : {p : α × α | dist p.1 p.2 < ε} ∈ 𝓤 α

Full source

/-- A constant size neighborhood of the diagonal is an entourage. -/
theorem dist_mem_uniformity {ε : ℝ} (ε0 : 0 < ε) : { p : α × α | dist p.1 p.2 < ε }{ p : α × α | dist p.1 p.2 < ε } ∈ 𝓤 α :=
  mem_uniformity_dist.2 ⟨ε, ε0, fun _ _ ↦ id⟩

$\varepsilon$-Neighborhood of Diagonal is an Entourage in Pseudometric Space

Informal description

For any positive real number $\varepsilon > 0$, the set $\{(a, b) \in \alpha \times \alpha \mid \text{dist}(a, b) < \varepsilon\}$ belongs to the uniformity filter $\mathfrak{U}(\alpha)$ of the pseudometric space $\alpha$.

Metric.uniformContinuous_iff theorem

 [PseudoMetricSpace β] {f : α → β} :
  UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b < δ → dist (f a) (f b) < ε

Full source

theorem uniformContinuous_iff [PseudoMetricSpace β] {f : α → β} :
    UniformContinuousUniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b < δ → dist (f a) (f b) < ε :=
  uniformity_basis_dist.uniformContinuous_iff uniformity_basis_dist

Uniform Continuity Criterion in Pseudometric Spaces via $\varepsilon$-$\delta$ Condition

Informal description

Let $\alpha$ and $\beta$ be pseudometric 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{dist}(a, b) < \delta$, we have $\text{dist}(f(a), f(b)) < \varepsilon$.

Metric.uniformContinuousOn_iff theorem

 [PseudoMetricSpace β] {f : α → β} {s : Set α} :
  UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y < δ → dist (f x) (f y) < ε

Full source

theorem uniformContinuousOn_iff [PseudoMetricSpace β] {f : α → β} {s : Set α} :
    UniformContinuousOnUniformContinuousOn f s ↔
      ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y < δ → dist (f x) (f y) < ε :=
  Metric.uniformity_basis_dist.uniformContinuousOn_iff Metric.uniformity_basis_dist

Uniform Continuity on Subset Criterion in Pseudometric Spaces

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, $f \colon \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset. Then $f$ is uniformly continuous on $s$ if and only if for every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $x, y \in s$, if $\text{dist}(x, y) < \delta$ then $\text{dist}(f(x), f(y)) < \varepsilon$.

Metric.uniformContinuousOn_iff_le theorem

 [PseudoMetricSpace β] {f : α → β} {s : Set α} :
  UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist (f x) (f y) ≤ ε

Full source

theorem uniformContinuousOn_iff_le [PseudoMetricSpace β] {f : α → β} {s : Set α} :
    UniformContinuousOnUniformContinuousOn f s ↔
      ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist (f x) (f y) ≤ ε :=
  Metric.uniformity_basis_dist_le.uniformContinuousOn_iff Metric.uniformity_basis_dist_le

Uniform Continuity on Subset via Closed Balls Criterion in Pseudometric Spaces

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, $f \colon \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset. Then $f$ is uniformly continuous on $s$ if and only if for every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $x, y \in s$ with $\text{dist}(x, y) \leq \delta$, we have $\text{dist}(f(x), f(y)) \leq \varepsilon$.

Metric.nhds_basis_ball theorem

: (𝓝 x).HasBasis (0 < ·) (ball x)

Full source

theorem nhds_basis_ball : (𝓝 x).HasBasis (0 < ·) (ball x) :=
  nhds_basis_uniformity uniformity_basis_dist

Neighborhood Basis via Open Balls in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of open balls $\text{ball}(x, \varepsilon)$ centered at $x$ with radius $\varepsilon > 0$.

Metric.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_ball.mem_iff

Neighborhood Characterization via Open Balls in Pseudometric Spaces

Informal description

A subset $s$ of a pseudometric space $\alpha$ is a neighborhood of a point $x \in \alpha$ if and only if there exists a positive real number $\varepsilon > 0$ such that the open ball $\text{ball}(x, \varepsilon)$ centered at $x$ with radius $\varepsilon$ is entirely contained in $s$.

Metric.eventually_nhds_iff theorem

{p : α → Prop} : (∀ᶠ y in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ ⦃y⦄, dist y x < ε → p y

Full source

theorem eventually_nhds_iff {p : α → Prop} :
    (∀ᶠ y in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ ⦃y⦄, dist y x < ε → p y :=
  mem_nhds_iff

Neighborhood Eventuality Characterization via Distance in Pseudometric Spaces

Informal description

For any predicate $p : \alpha \to \text{Prop}$ and any point $x$ in a pseudometric space $\alpha$, the predicate $p(y)$ holds for all $y$ in some neighborhood of $x$ if and only if there exists $\varepsilon > 0$ such that $p(y)$ holds for all $y$ with $\text{dist}(y, x) < \varepsilon$.

Metric.eventually_nhds_iff_ball theorem

{p : α → Prop} : (∀ᶠ y in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ y ∈ ball x ε, p y

Full source

theorem eventually_nhds_iff_ball {p : α → Prop} :
    (∀ᶠ y in 𝓝 x, p y) ↔ ∃ ε > 0, ∀ y ∈ ball x ε, p y :=
  mem_nhds_iff

Neighborhood Characterization via Open Balls for Predicates in Pseudometric Spaces

Informal description

For a pseudometric space $\alpha$, a point $x \in \alpha$, and a predicate $p : \alpha \to \mathrm{Prop}$, the following are equivalent: 1. The predicate $p(y)$ holds for all $y$ in some neighborhood of $x$. 2. There exists $\varepsilon > 0$ such that $p(y)$ holds for all $y$ in the open ball $\mathrm{ball}(x, \varepsilon)$.

Metric.eventually_nhds_prod_iff theorem

 {f : Filter ι} {x₀ : α} {p : α × ι → Prop} :
  (∀ᶠ x in 𝓝 x₀ ×ˢ f, p x) ↔
    ∃ ε > (0 : ℝ), ∃ pa : ι → Prop, (∀ᶠ i in f, pa i) ∧ ∀ ⦃x⦄, dist x x₀ < ε → ∀ ⦃i⦄, pa i → p (x, i)

Full source

/-- A version of `Filter.eventually_prod_iff` where the first filter consists of neighborhoods
in a pseudo-metric space. -/
theorem eventually_nhds_prod_iff {f : Filter ι} {x₀ : α} {p : α × ι → Prop} :
    (∀ᶠ x in 𝓝 x₀ ×ˢ f, p x) ↔ ∃ ε > (0 : ℝ), ∃ pa : ι → Prop, (∀ᶠ i in f, pa i) ∧
      ∀ ⦃x⦄, dist x x₀ < ε → ∀ ⦃i⦄, pa i → p (x, i) := by
  refine (nhds_basis_ball.prod f.basis_sets).eventually_iff.trans ?_
  simp only [Prod.exists, forall_prod_set, id, mem_ball, and_assoc, exists_and_left, and_imp]
  rfl

Characterization of Eventually in Product Neighborhood in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $x_0 \in \alpha$, $f$ a filter on a type $\iota$, and $p : \alpha \times \iota \to \mathrm{Prop}$ a predicate. Then the following are equivalent: 1. The predicate $p(x,i)$ holds for all $(x,i)$ in some neighborhood of $x_0$ in $\alpha$ times some set in $f$. 2. There exists $\varepsilon > 0$ and a predicate $pa : \iota \to \mathrm{Prop}$ such that: - $pa(i)$ holds for all $i$ in some set in $f$, - For all $x \in \alpha$ with $\mathrm{dist}(x,x_0) < \varepsilon$ and all $i \in \iota$ satisfying $pa(i)$, the predicate $p(x,i)$ holds.

Metric.eventually_prod_nhds_iff theorem

 {f : Filter ι} {x₀ : α} {p : ι × α → Prop} :
  (∀ᶠ x in f ×ˢ 𝓝 x₀, p x) ↔ ∃ pa : ι → Prop, (∀ᶠ i in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i⦄, pa i → ∀ ⦃x⦄, dist x x₀ < ε → p (i, x)

Full source

/-- A version of `Filter.eventually_prod_iff` where the second filter consists of neighborhoods
in a pseudo-metric space. -/
theorem eventually_prod_nhds_iff {f : Filter ι} {x₀ : α} {p : ι × α → Prop} :
    (∀ᶠ x in f ×ˢ 𝓝 x₀, p x) ↔ ∃ pa : ι → Prop, (∀ᶠ i in f, pa i) ∧
      ∃ ε > 0, ∀ ⦃i⦄, pa i → ∀ ⦃x⦄, dist x x₀ < ε → p (i, x) := by
  rw [eventually_swap_iff, Metric.eventually_nhds_prod_iff]
  constructor <;>
    · rintro ⟨a1, a2, a3, a4, a5⟩
      exact ⟨a3, a4, a1, a2, fun _ b1 b2 b3 => a5 b3 b1⟩

Characterization of Eventually in Product Filter-Neighborhood in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $x_0 \in \alpha$, $f$ a filter on a type $\iota$, and $p : \iota \times \alpha \to \mathrm{Prop}$ a predicate. Then the following are equivalent: 1. The predicate $p(i,x)$ holds for all $(i,x)$ in some set in $f$ times a neighborhood of $x_0$ in $\alpha$. 2. There exists a predicate $pa : \iota \to \mathrm{Prop}$ and $\varepsilon > 0$ such that: - $pa(i)$ holds for all $i$ in some set in $f$, - For all $i \in \iota$ satisfying $pa(i)$ and all $x \in \alpha$ with $\mathrm{dist}(x,x_0) < \varepsilon$, the predicate $p(i,x)$ holds.

Metric.nhds_basis_closedBall theorem

: (𝓝 x).HasBasis (fun ε : ℝ => 0 < ε) (closedBall x)

Full source

theorem nhds_basis_closedBall : (𝓝 x).HasBasis (fun ε : ℝ => 0 < ε) (closedBall x) :=
  nhds_basis_uniformity uniformity_basis_dist_le

Neighborhood Basis via Closed Balls in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of closed balls $\overline{B}(x, \varepsilon)$ centered at $x$ with radius $\varepsilon > 0$.

Metric.nhds_basis_ball_inv_nat_succ theorem

: (𝓝 x).HasBasis (fun _ => True) fun n : ℕ => ball x (1 / (↑n + 1))

Full source

theorem nhds_basis_ball_inv_nat_succ :
    (𝓝 x).HasBasis (fun _ => True) fun n : ℕ => ball x (1 / (↑n + 1)) :=
  nhds_basis_uniformity uniformity_basis_dist_inv_nat_succ

Neighborhood Basis via Open Balls with Reciprocal Successor Radii in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of open balls $B(x, \frac{1}{n+1})$ centered at $x$ with radius $\frac{1}{n+1}$ for all natural numbers $n \in \mathbb{N}$.

Metric.nhds_basis_ball_inv_nat_pos theorem

: (𝓝 x).HasBasis (fun n => 0 < n) fun n : ℕ => ball x (1 / ↑n)

Full source

theorem nhds_basis_ball_inv_nat_pos :
    (𝓝 x).HasBasis (fun n => 0 < n) fun n : ℕ => ball x (1 / ↑n) :=
  nhds_basis_uniformity uniformity_basis_dist_inv_nat_pos

Neighborhood Basis via Inverse Natural Number Radii in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of open balls $B(x, \frac{1}{n})$ centered at $x$ with radius $\frac{1}{n}$ for all positive natural numbers $n \in \mathbb{N}$.

Metric.nhds_basis_ball_pow theorem

{r : ℝ} (h0 : 0 < r) (h1 : r < 1) : (𝓝 x).HasBasis (fun _ => True) fun n : ℕ => ball x (r ^ n)

Full source

theorem nhds_basis_ball_pow {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
    (𝓝 x).HasBasis (fun _ => True) fun n : ℕ => ball x (r ^ n) :=
  nhds_basis_uniformity (uniformity_basis_dist_pow h0 h1)

Neighborhood Basis via Powers of $r$ in Pseudometric Spaces for $0 < r < 1$

Informal description

Let $\alpha$ be a pseudometric space and let $r \in \mathbb{R}$ satisfy $0 < r < 1$. Then the neighborhood filter $\mathcal{N}(x)$ at any point $x \in \alpha$ has a basis consisting of the open balls $\text{ball}(x, r^n)$ for all natural numbers $n \in \mathbb{N}$.

Metric.nhds_basis_closedBall_pow theorem

{r : ℝ} (h0 : 0 < r) (h1 : r < 1) : (𝓝 x).HasBasis (fun _ => True) fun n : ℕ => closedBall x (r ^ n)

Full source

theorem nhds_basis_closedBall_pow {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
    (𝓝 x).HasBasis (fun _ => True) fun n : ℕ => closedBall x (r ^ n) :=
  nhds_basis_uniformity (uniformity_basis_dist_le_pow h0 h1)

Neighborhood basis via geometric sequence of closed balls in pseudometric spaces

Informal description

Let $\alpha$ be a pseudometric space and $x \in \alpha$. For any real number $r$ satisfying $0 < r < 1$, the neighborhood filter $\mathcal{N}(x)$ has a basis consisting of the closed balls $\overline{B}(x, r^n)$ for all natural numbers $n \in \mathbb{N}$.

Metric.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 only [isOpen_iff_mem_nhds, mem_nhds_iff]

Characterization of Open Sets in Pseudometric Spaces via Open Balls

Informal description

A subset $s$ of a pseudometric space $\alpha$ is open if and only if for every point $x \in s$, there exists a positive real number $\varepsilon$ such that the open ball $\text{ball}(x, \varepsilon)$ is entirely contained in $s$.

Metric.isOpen_ball theorem

: IsOpen (ball x ε)

Full source

@[simp] theorem isOpen_ball : IsOpen (ball x ε) :=
  isOpen_iff.2 fun _ => exists_ball_subset_ball

Open Balls are Open Sets in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon$, the open ball $\text{ball}(x, \varepsilon) = \{ y \mid \text{dist}(y, x) < \varepsilon \}$ is an open set.

Metric.ball_mem_nhds theorem

(x : α) {ε : ℝ} (ε0 : 0 < ε) : ball x ε ∈ 𝓝 x

Full source

theorem ball_mem_nhds (x : α) {ε : ℝ} (ε0 : 0 < ε) : ballball x ε ∈ 𝓝 x :=
  isOpen_ball.mem_nhds (mem_ball_self ε0)

Open Balls are Neighborhoods in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon > 0$, the open ball $\text{ball}(x, \varepsilon) = \{ y \mid \text{dist}(y, x) < \varepsilon \}$ is a neighborhood of $x$ in the topology induced by the pseudometric.

Metric.closedBall_mem_nhds theorem

(x : α) {ε : ℝ} (ε0 : 0 < ε) : closedBall x ε ∈ 𝓝 x

Full source

theorem closedBall_mem_nhds (x : α) {ε : ℝ} (ε0 : 0 < ε) : closedBallclosedBall x ε ∈ 𝓝 x :=
  mem_of_superset (ball_mem_nhds x ε0) ball_subset_closedBall

Closed Balls are Neighborhoods in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon > 0$, the closed ball $\overline{B}(x, \varepsilon) = \{ y \mid \text{dist}(y, x) \leq \varepsilon \}$ is a neighborhood of $x$ in the topology induced by the pseudometric.

Metric.closedBall_mem_nhds_of_mem theorem

{x c : α} {ε : ℝ} (h : x ∈ ball c ε) : closedBall c ε ∈ 𝓝 x

Full source

theorem closedBall_mem_nhds_of_mem {x c : α} {ε : ℝ} (h : x ∈ ball c ε) : closedBallclosedBall c ε ∈ 𝓝 x :=
  mem_of_superset (isOpen_ball.mem_nhds h) ball_subset_closedBall

Closed Ball is Neighborhood of Points in Open Ball

Informal description

For any points $x, c$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon$, if $x$ belongs to the open ball $B(c, \varepsilon)$, then the closed ball $\overline{B}(c, \varepsilon)$ is a neighborhood of $x$.

Metric.nhdsWithin_basis_ball theorem

{s : Set α} : (𝓝[s] x).HasBasis (fun ε : ℝ => 0 < ε) fun ε => ball x ε ∩ s

Full source

theorem nhdsWithin_basis_ball {s : Set α} :
    (𝓝[s] x).HasBasis (fun ε : ℝ => 0 < ε) fun ε => ballball x ε ∩ s :=
  nhdsWithin_hasBasis nhds_basis_ball s

Basis for Relative Neighborhood Filter via Open Balls in Pseudometric Spaces

Informal description

For any subset $s$ of a pseudometric space $\alpha$ and any point $x \in \alpha$, the relative neighborhood filter $\mathcal{N}_s(x)$ (neighborhoods of $x$ within $s$) has a basis consisting of sets of the form $B(x, \varepsilon) \cap s$ where $\varepsilon > 0$ and $B(x, \varepsilon)$ is the open ball centered at $x$ with radius $\varepsilon$.

Metric.mem_nhdsWithin_iff theorem

{t : Set α} : s ∈ 𝓝[t] x ↔ ∃ ε > 0, ball x ε ∩ t ⊆ s

Full source

theorem mem_nhdsWithin_iff {t : Set α} : s ∈ 𝓝[t] xs ∈ 𝓝[t] x ↔ ∃ ε > 0, ball x ε ∩ t ⊆ s :=
  nhdsWithin_basis_ball.mem_iff

Characterization of Relative Neighborhoods via Open Balls in Pseudometric Spaces

Informal description

For a subset $s$ of a pseudometric space $\alpha$ and a point $x \in \alpha$, the set $s$ is a neighborhood of $x$ within $t$ (denoted $s \in \mathcal{N}_t(x)$) if and only if there exists $\varepsilon > 0$ such that the intersection of the open ball $B(x, \varepsilon)$ with $t$ is contained in $s$.

Metric.tendsto_nhdsWithin_nhdsWithin theorem

 [PseudoMetricSpace β] {t : Set β} {f : α → β} {a b} :
  Tendsto f (𝓝[s] a) (𝓝[t] b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε

Full source

theorem tendsto_nhdsWithin_nhdsWithin [PseudoMetricSpace β] {t : Set β} {f : α → β} {a b} :
    TendstoTendsto f (𝓝[s] a) (𝓝[t] b) ↔
      ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε :=
  (nhdsWithin_basis_ball.tendsto_iff nhdsWithin_basis_ball).trans <| by
    simp only [inter_comm _ s, inter_comm _ t, mem_inter_iff, and_imp, gt_iff_lt, mem_ball]

$\varepsilon$-$\delta$ Characterization of Relative Limits in Pseudometric Spaces

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, $s \subseteq \alpha$, $t \subseteq \beta$, $f : \alpha \to \beta$ a function, and $a \in \alpha$, $b \in \beta$. The function $f$ tends to $b$ within $t$ as $x$ approaches $a$ within $s$ if and only if for every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $x \in s$ with $\text{dist}(x, a) < \delta$, we have $f(x) \in t$ and $\text{dist}(f(x), b) < \varepsilon$.

Metric.tendsto_nhdsWithin_nhds theorem

 [PseudoMetricSpace β] {f : α → β} {a b} :
  Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε

Full source

theorem tendsto_nhdsWithin_nhds [PseudoMetricSpace β] {f : α → β} {a b} :
    TendstoTendsto f (𝓝[s] a) (𝓝 b) ↔
      ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε := by
  rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]
  simp only [mem_univ, true_and]

$\varepsilon$-$\delta$ Characterization of Relative Limits in Pseudometric Spaces

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, $s \subseteq \alpha$, $f : \alpha \to \beta$ a function, and $a \in \alpha$, $b \in \beta$. The function $f$ tends to $b$ as $x$ approaches $a$ within $s$ if and only if for every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $x \in s$ with $\text{dist}(x, a) < \delta$, we have $\text{dist}(f(x), b) < \varepsilon$.

Metric.tendsto_nhds_nhds theorem

 [PseudoMetricSpace β] {f : α → β} {a b} :
  Tendsto f (𝓝 a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) b < ε

Full source

theorem tendsto_nhds_nhds [PseudoMetricSpace β] {f : α → β} {a b} :
    TendstoTendsto f (𝓝 a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) b < ε :=
  nhds_basis_ball.tendsto_iff nhds_basis_ball

$\varepsilon$-$\delta$ Characterization of Limit in Pseudometric Spaces

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f : \alpha \to \beta$ be a function. For any points $a \in \alpha$ and $b \in \beta$, the function $f$ tends to $b$ as $x$ approaches $a$ (i.e., $\lim_{x \to a} f(x) = b$) if and only if for every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $x \in \alpha$, if $\text{dist}(x, a) < \delta$, then $\text{dist}(f(x), b) < \varepsilon$.

Metric.continuousAt_iff theorem

 [PseudoMetricSpace β] {f : α → β} {a : α} :
  ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε

Full source

theorem continuousAt_iff [PseudoMetricSpace β] {f : α → β} {a : α} :
    ContinuousAtContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε := by
  rw [ContinuousAt, tendsto_nhds_nhds]

$\varepsilon$-$\delta$ Characterization of Continuity at a Point in Pseudometric Spaces

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces and $f : \alpha \to \beta$ a function. For any point $a \in \alpha$, $f$ is continuous at $a$ if and only if for every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $x \in \alpha$ with $\text{dist}(x, a) < \delta$, we have $\text{dist}(f(x), f(a)) < \varepsilon$.

Metric.continuousWithinAt_iff theorem

 [PseudoMetricSpace β] {f : α → β} {a : α} {s : Set α} :
  ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε

Full source

theorem continuousWithinAt_iff [PseudoMetricSpace β] {f : α → β} {a : α} {s : Set α} :
    ContinuousWithinAtContinuousWithinAt f s a ↔
      ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε := by
  rw [ContinuousWithinAt, tendsto_nhdsWithin_nhds]

$\varepsilon$-$\delta$ Characterization of Continuity at a Point Relative to a Subset in Pseudometric Spaces

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, $f : \alpha \to \beta$ a function, $s \subseteq \alpha$ a subset, and $a \in \alpha$ a point. The function $f$ is continuous at $a$ within $s$ if and only if for every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $x \in s$ with $\text{dist}(x, a) < \delta$, we have $\text{dist}(f(x), f(a)) < \varepsilon$.

Metric.continuousOn_iff theorem

 [PseudoMetricSpace β] {f : α → β} {s : Set α} :
  ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε

Full source

theorem continuousOn_iff [PseudoMetricSpace β] {f : α → β} {s : Set α} :
    ContinuousOnContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε := by
  simp [ContinuousOn, continuousWithinAt_iff]

Characterization of Continuity on a Subset in Pseudometric Spaces

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, $f : \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset. Then $f$ is continuous on $s$ if and only if for every point $b \in s$ and every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $a \in s$ with $\text{dist}(a, b) < \delta$, we have $\text{dist}(f(a), f(b)) < \varepsilon$.

Metric.continuous_iff theorem

 [PseudoMetricSpace β] {f : α → β} : Continuous f ↔ ∀ b, ∀ ε > 0, ∃ δ > 0, ∀ a, dist a b < δ → dist (f a) (f b) < ε

Full source

theorem continuous_iff [PseudoMetricSpace β] {f : α → β} :
    ContinuousContinuous f ↔ ∀ b, ∀ ε > 0, ∃ δ > 0, ∀ a, dist a b < δ → dist (f a) (f b) < ε :=
  continuous_iff_continuousAt.trans <| forall_congr' fun _ => tendsto_nhds_nhds

$\varepsilon$-$\delta$ Characterization of Continuity in Pseudometric Spaces

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces and $f : \alpha \to \beta$ a function. Then $f$ is continuous if and only if for every point $b \in \alpha$ and every $\varepsilon > 0$, there exists $\delta > 0$ such that for all $a \in \alpha$ with $\text{dist}(a, b) < \delta$, we have $\text{dist}(f(a), f(b)) < \varepsilon$.

Metric.tendsto_nhds theorem

{f : Filter β} {u : β → α} {a : α} : Tendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, dist (u x) a < ε

Full source

theorem tendsto_nhds {f : Filter β} {u : β → α} {a : α} :
    TendstoTendsto u f (𝓝 a) ↔ ∀ ε > 0, ∀ᶠ x in f, dist (u x) a < ε :=
  nhds_basis_ball.tendsto_right_iff

Characterization of Convergence in Pseudometric Spaces via Open Balls

Informal description

Let $\alpha$ be a pseudometric space, $f$ a filter on a type $\beta$, and $u : \beta \to \alpha$ a function. Then $u$ converges to a point $a \in \alpha$ with respect to the filter $f$ if and only if for every $\varepsilon > 0$, the set $\{x \in \beta \mid \text{dist}(u(x), a) < \varepsilon\}$ is eventually in $f$.

Metric.continuousAt_iff' theorem

 [TopologicalSpace β] {f : β → α} {b : β} : ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ x in 𝓝 b, dist (f x) (f b) < ε

Full source

theorem continuousAt_iff' [TopologicalSpace β] {f : β → α} {b : β} :
    ContinuousAtContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ x in 𝓝 b, dist (f x) (f b) < ε := by
  rw [ContinuousAt, tendsto_nhds]

Characterization of Continuity at a Point in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $\beta$ be a topological space. A function $f : \beta \to \alpha$ is continuous at a point $b \in \beta$ if and only if for every $\varepsilon > 0$, there exists a neighborhood $U$ of $b$ such that for all $x \in U$, the distance between $f(x)$ and $f(b)$ is less than $\varepsilon$.

Metric.continuousWithinAt_iff' theorem

 [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
  ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ x in 𝓝[s] b, dist (f x) (f b) < ε

Full source

theorem continuousWithinAt_iff' [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
    ContinuousWithinAtContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ x in 𝓝[s] b, dist (f x) (f b) < ε := by
  rw [ContinuousWithinAt, tendsto_nhds]

Characterization of Continuity at a Point within a Subset in Pseudometric Spaces

Informal description

Let $X$ be a topological space, $f : X \to \alpha$ a function from $X$ to a pseudometric space $\alpha$, $b \in X$ a point, and $s \subseteq X$ a subset. Then $f$ is continuous at $b$ within $s$ if and only if for every $\varepsilon > 0$, there exists a neighborhood $U$ of $b$ in $s$ such that for all $x \in U$, the distance between $f(x)$ and $f(b)$ is less than $\varepsilon$.

Metric.continuousOn_iff' theorem

 [TopologicalSpace β] {f : β → α} {s : Set β} :
  ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ x in 𝓝[s] b, dist (f x) (f b) < ε

Full source

theorem continuousOn_iff' [TopologicalSpace β] {f : β → α} {s : Set β} :
    ContinuousOnContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ x in 𝓝[s] b, dist (f x) (f b) < ε := by
  simp [ContinuousOn, continuousWithinAt_iff']

Characterization of Continuity on Subsets in Pseudometric Spaces

Informal description

Let $X$ be a topological space and $f : X \to \alpha$ be a function from $X$ to a pseudometric space $\alpha$. Then $f$ is continuous on a subset $s \subseteq X$ if and only if for every point $b \in s$ and every $\epsilon > 0$, there exists a neighborhood of $b$ within $s$ such that for all $x$ in this neighborhood, the distance between $f(x)$ and $f(b)$ is less than $\epsilon$. In other words: \[ \text{ContinuousOn } f s \leftrightarrow \forall b \in s, \forall \epsilon > 0, \exists U \in \mathcal{N}_s(b), \forall x \in U, \text{dist}(f(x), f(b)) < \epsilon \] where $\mathcal{N}_s(b)$ denotes the neighborhood filter of $b$ within $s$.

Metric.continuous_iff' theorem

[TopologicalSpace β] {f : β → α} : Continuous f ↔ ∀ (a), ∀ ε > 0, ∀ᶠ x in 𝓝 a, dist (f x) (f a) < ε

Full source

theorem continuous_iff' [TopologicalSpace β] {f : β → α} :
    ContinuousContinuous f ↔ ∀ (a), ∀ ε > 0, ∀ᶠ x in 𝓝 a, dist (f x) (f a) < ε :=
  continuous_iff_continuousAt.trans <| forall_congr' fun _ => tendsto_nhds

Characterization of Continuity in Pseudometric Spaces via Open Balls

Informal description

Let $X$ be a topological space and $\alpha$ be a pseudometric space. A function $f : X \to \alpha$ is continuous if and only if for every point $a \in X$ and every $\epsilon > 0$, there exists a neighborhood of $a$ such that for all $x$ in this neighborhood, the distance between $f(x)$ and $f(a)$ is less than $\epsilon$. In other words: \[ f \text{ is continuous} \leftrightarrow \forall a \in X, \forall \epsilon > 0, \exists U \in \mathcal{N}(a), \forall x \in U, \text{dist}(f(x), f(a)) < \epsilon \] where $\mathcal{N}(a)$ denotes the neighborhood filter of $a$.

Metric.tendsto_atTop theorem

 [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} : Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε

Full source

theorem tendsto_atTop [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} :
    TendstoTendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) a < ε :=
  (atTop_basis.tendsto_iff nhds_basis_ball).trans <| by
    simp only [true_and, mem_ball, mem_Ici]

Convergence Criterion for Sequences in Pseudometric Spaces via Directed Sets

Informal description

Let $\alpha$ be a pseudometric space and $\beta$ be a nonempty directed set (join-semilattice). A sequence $u : \beta \to \alpha$ converges to a point $a \in \alpha$ if and only if for every $\epsilon > 0$, there exists an index $N \in \beta$ such that for all $n \geq N$, the distance between $u(n)$ and $a$ is less than $\epsilon$, i.e., $\text{dist}(u(n), a) < \epsilon$.

Metric.tendsto_atTop' theorem

 [Nonempty β] [SemilatticeSup β] [NoMaxOrder β] {u : β → α} {a : α} :
  Tendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n > N, dist (u n) a < ε

Full source

/-- A variant of `tendsto_atTop` that
uses `∃ N, ∀ n > N, ...` rather than `∃ N, ∀ n ≥ N, ...`
-/
theorem tendsto_atTop' [Nonempty β] [SemilatticeSup β] [NoMaxOrder β] {u : β → α} {a : α} :
    TendstoTendsto u atTop (𝓝 a) ↔ ∀ ε > 0, ∃ N, ∀ n > N, dist (u n) a < ε :=
  (atTop_basis_Ioi.tendsto_iff nhds_basis_ball).trans <| by
    simp only [true_and, gt_iff_lt, mem_Ioi, mem_ball]

Convergence Criterion for Sequences in Pseudometric Spaces via Strictly Increasing Indices

Informal description

Let $\alpha$ be a pseudometric space and $\beta$ be a nonempty directed set (join-semilattice) with no maximal element. A sequence $u : \beta \to \alpha$ converges to a point $a \in \alpha$ if and only if for every $\epsilon > 0$, there exists an index $N \in \beta$ such that for all $n > N$, the distance between $u(n)$ and $a$ is less than $\epsilon$, i.e., $\text{dist}(u(n), a) < \epsilon$.

Metric.isOpen_singleton_iff theorem

{α : Type*} [PseudoMetricSpace α] {x : α} : IsOpen ({ x } : Set α) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x

Full source

theorem isOpen_singleton_iff {α : Type*} [PseudoMetricSpace α] {x : α} :
    IsOpenIsOpen ({x} : Set α) ↔ ∃ ε > 0, ∀ y, dist y x < ε → y = x := by
  simp [isOpen_iff, subset_singleton_iff, mem_ball]

Characterization of Open Singleton Sets in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, a singleton set $\{x\}$ is open if and only if there exists a positive real number $\varepsilon$ such that for every point $y$ in $\alpha$, if the distance between $y$ and $x$ is less than $\varepsilon$, then $y$ must equal $x$. In other words, $\{x\}$ is open precisely when $x$ is an isolated point of the space.

Dense.exists_dist_lt theorem

{s : Set α} (hs : Dense s) (x : α) {ε : ℝ} (hε : 0 < ε) : ∃ y ∈ s, dist x y < ε

Full source

theorem _root_.Dense.exists_dist_lt {s : Set α} (hs : Dense s) (x : α) {ε : ℝ} (hε : 0 < ε) :
    ∃ y ∈ s, dist x y < ε := by
  have : (ball x ε).Nonempty := by simp [hε]
  simpa only [mem_ball'] using hs.exists_mem_open isOpen_ball this

Existence of Points in Dense Sets Arbitrarily Close to Any Given Point

Informal description

For any dense subset $s$ of a pseudometric space $\alpha$, any point $x \in \alpha$, and any positive real number $\varepsilon > 0$, there exists a point $y \in s$ such that the distance between $x$ and $y$ is less than $\varepsilon$, i.e., $\text{dist}(x, y) < \varepsilon$.

DenseRange.exists_dist_lt theorem

{β : Type*} {f : β → α} (hf : DenseRange f) (x : α) {ε : ℝ} (hε : 0 < ε) : ∃ y, dist x (f y) < ε

Full source

nonrec theorem _root_.DenseRange.exists_dist_lt {β : Type*} {f : β → α} (hf : DenseRange f) (x : α)
    {ε : ℝ} (hε : 0 < ε) : ∃ y, dist x (f y) < ε :=
  exists_range_iff.1 (hf.exists_dist_lt x hε)

Existence of Points in Dense Range Arbitrarily Close to Any Given Point

Informal description

For any function $f \colon \beta \to \alpha$ with dense range in a pseudometric space $\alpha$, any point $x \in \alpha$, and any positive real number $\varepsilon > 0$, there exists an element $y \in \beta$ such that the distance between $x$ and $f(y)$ is less than $\varepsilon$, i.e., $\text{dist}(x, f(y)) < \varepsilon$.

Metric.uniformSpace_eq_bot theorem

 : ‹PseudoMetricSpace α›.toUniformSpace = ⊥ ↔ ∃ r : ℝ, 0 < r ∧ Pairwise (r ≤ dist · · : α → α → Prop)

Full source

/-- (Pseudo) metric space has discrete `UniformSpace` structure
iff the distances between distinct points are uniformly bounded away from zero. -/
protected lemma uniformSpace_eq_bot :
    ‹PseudoMetricSpace α›.toUniformSpace = ⊥ ↔
      ∃ r : ℝ, 0 < r ∧ Pairwise (r ≤ dist · · : α → α → Prop) := by
  simp only [uniformity_basis_dist.uniformSpace_eq_bot, mem_setOf_eq, not_lt]

Discrete Uniformity Criterion for Pseudometric Spaces via Uniformly Bounded Distances

Informal description

The uniform space structure induced by a pseudometric space $\alpha$ is discrete (i.e., equal to the trivial uniform space structure $\bot$) if and only if there exists a positive real number $r > 0$ such that the distance between any two distinct points in $\alpha$ is at least $r$.

DiscreteTopology.of_forall_le_dist theorem

 {α} [PseudoMetricSpace α] {r : ℝ} (hpos : 0 < r) (hr : Pairwise (r ≤ dist · · : α → α → Prop)) : DiscreteTopology α

Full source

/-- If the distances between distinct points in a (pseudo) metric space
are uniformly bounded away from zero, then the space has discrete topology. -/
lemma DiscreteTopology.of_forall_le_dist {α} [PseudoMetricSpace α] {r : ℝ} (hpos : 0 < r)
    (hr : Pairwise (r ≤ dist · · : α → α → Prop)) : DiscreteTopology α :=
  ⟨by rw [Metric.uniformSpace_eq_bot.2 ⟨r, hpos, hr⟩, UniformSpace.toTopologicalSpace_bot]⟩

Discrete Topology Criterion via Uniformly Bounded Distances in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space. If there exists a positive real number $r > 0$ such that the distance between any two distinct points in $\alpha$ is at least $r$, then $\alpha$ has the discrete topology (i.e., every subset of $\alpha$ is open).

Metric.uniformity_edist_aux theorem

 {α} (d : α → α → ℝ≥0) :
  ⨅ ε > (0 : ℝ), 𝓟 {p : α × α | ↑(d p.1 p.2) < ε} = ⨅ ε > (0 : ℝ≥0∞), 𝓟 {p : α × α | ↑(d p.1 p.2) < ε}

Full source

theorem Metric.uniformity_edist_aux {α} (d : α → α → ℝ≥0) :
    ⨅ ε > (0 : ℝ), 𝓟 { p : α × α | ↑(d p.1 p.2) < ε } =
      ⨅ ε > (0 : ℝ≥0∞), 𝓟 { p : α × α | ↑(d p.1 p.2) < ε } := by
  simp only [le_antisymm_iff, le_iInf_iff, le_principal_iff]
  refine ⟨fun ε hε => ?_, fun ε hε => ?_⟩
  · rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hε with ⟨ε', ε'0, ε'ε⟩
    refine mem_iInf_of_mem (ε' : ℝ) (mem_iInf_of_mem (ENNReal.coe_pos.1 ε'0) ?_)
    exact fun x hx => lt_trans (ENNReal.coe_lt_coe.2 hx) ε'ε
  · lift ε to ℝ≥0 using le_of_lt hε
    refine mem_iInf_of_mem (ε : ℝ≥0∞) (mem_iInf_of_mem (ENNReal.coe_pos.2 hε) ?_)
    exact fun _ => ENNReal.coe_lt_coe.1

Equality of Uniformity Filters via Real and Extended Nonnegative Distance Conditions

Informal description

Let $\alpha$ be a type and $d : \alpha \to \alpha \to \mathbb{R}_{\geq 0}$ be a distance function. Then the infimum over all positive real numbers $\varepsilon$ of the principal filter generated by the set $\{(x, y) \mid d(x, y) < \varepsilon\}$ is equal to the infimum over all positive extended nonnegative real numbers $\varepsilon$ of the principal filter generated by the set $\{(x, y) \mid d(x, y) < \varepsilon\}$.

Metric.uniformity_edist theorem

: 𝓤 α = ⨅ ε > 0, 𝓟 {p : α × α | edist p.1 p.2 < ε}

Full source

theorem Metric.uniformity_edist : 𝓤 α = ⨅ ε > 0, 𝓟 { p : α × α | edist p.1 p.2 < ε } := by
  simp only [PseudoMetricSpace.uniformity_dist, dist_nndist, edist_nndist,
    Metric.uniformity_edist_aux]

Uniformity Filter Characterization via Extended Distance in Pseudometric Spaces

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ on a pseudometric space $\alpha$ is equal to the infimum over all positive real numbers $\varepsilon$ of the principal filter generated by the set $\{(x, y) \mid \text{edist}(x, y) < \varepsilon\}$, where $\text{edist}$ is the extended distance function on $\alpha$.

PseudoMetricSpace.toPseudoEMetricSpace instance

: PseudoEMetricSpace α

Full source

/-- A pseudometric space induces a pseudoemetric space -/
instance (priority := 100) PseudoMetricSpace.toPseudoEMetricSpace : PseudoEMetricSpace α :=
  { ‹PseudoMetricSpace α› with
    edist_self := by simp [edist_dist]
    edist_comm := fun _ _ => by simp only [edist_dist, dist_comm]
    edist_triangle := fun x y z => by
      simp only [edist_dist, ← ENNReal.ofReal_add, dist_nonneg]
      rw [ENNReal.ofReal_le_ofReal_iff _]
      · exact dist_triangle _ _ _
      · simpa using add_le_add (dist_nonneg : 0 ≤ dist x y) dist_nonneg
    uniformity_edist := Metric.uniformity_edist }

Pseudometric Space Induces Pseudoemetric Space

Informal description

Every pseudometric space $\alpha$ can be naturally endowed with a pseudoemetric space structure, where the extended distance function is derived from the original distance function.

Metric.eball_top_eq_univ theorem

(x : α) : EMetric.ball x ∞ = Set.univ

Full source

/-- In a pseudometric space, an open ball of infinite radius is the whole space -/
theorem Metric.eball_top_eq_univ (x : α) : EMetric.ball x ∞ = Set.univ :=
  Set.eq_univ_iff_forall.mpr fun y => edist_lt_top y x

Open Ball with Infinite Radius is the Whole Space in Pseudometric Spaces

Informal description

In a pseudometric space $\alpha$, for any point $x \in \alpha$, the open ball centered at $x$ with infinite radius is equal to the entire space, i.e., $B(x, \infty) = \alpha$.

Metric.emetric_ball theorem

{x : α} {ε : ℝ} : EMetric.ball x (ENNReal.ofReal ε) = ball x ε

Full source

/-- Balls defined using the distance or the edistance coincide -/
@[simp]
theorem Metric.emetric_ball {x : α} {ε : ℝ} : EMetric.ball x (ENNReal.ofReal ε) = ball x ε := by
  ext y
  simp only [EMetric.mem_ball, mem_ball, edist_dist]
  exact ENNReal.ofReal_lt_ofReal_iff_of_nonneg dist_nonneg

Equality of Open Balls Defined via Standard and Extended Distance Functions

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $\varepsilon$, the open ball defined using the extended distance function $\text{edist}$ coincides with the open ball defined using the standard distance function $\text{dist}$. That is, $\text{EMetric.ball}(x, \text{ENNReal.ofReal}(\varepsilon)) = \text{ball}(x, \varepsilon)$.

Metric.emetric_ball_nnreal theorem

{x : α} {ε : ℝ≥0} : EMetric.ball x ε = ball x ε

Full source

/-- Balls defined using the distance or the edistance coincide -/
@[simp]
theorem Metric.emetric_ball_nnreal {x : α} {ε : ℝ≥0} : EMetric.ball x ε = ball x ε := by
  rw [← Metric.emetric_ball]
  simp

Equality of Open Balls via Standard and Extended Distance for Nonnegative Radii

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any nonnegative real number $\varepsilon \in \mathbb{R}_{\geq 0}$, the open ball defined using the extended distance function $\text{edist}$ coincides with the open ball defined using the standard distance function $\text{dist}$. That is, $\text{EMetric.ball}(x, \varepsilon) = \text{ball}(x, \varepsilon)$.

Metric.emetric_closedBall theorem

{x : α} {ε : ℝ} (h : 0 ≤ ε) : EMetric.closedBall x (ENNReal.ofReal ε) = closedBall x ε

Full source

/-- Closed balls defined using the distance or the edistance coincide -/
theorem Metric.emetric_closedBall {x : α} {ε : ℝ} (h : 0 ≤ ε) :
    EMetric.closedBall x (ENNReal.ofReal ε) = closedBall x ε := by
  ext y; simp [edist_le_ofReal h]

Equality of Closed Balls via Standard and Extended Distance

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon \geq 0$, the closed ball defined using the extended distance function coincides with the closed ball defined using the standard distance function. That is: \[ \text{EMetric.closedBall}(x, \text{ENNReal.ofReal}(\varepsilon)) = \text{closedBall}(x, \varepsilon) \]

Metric.emetric_closedBall_nnreal theorem

{x : α} {ε : ℝ≥0} : EMetric.closedBall x ε = closedBall x ε

Full source

/-- Closed balls defined using the distance or the edistance coincide -/
@[simp]
theorem Metric.emetric_closedBall_nnreal {x : α} {ε : ℝ≥0} :
    EMetric.closedBall x ε = closedBall x ε := by
  rw [← Metric.emetric_closedBall ε.coe_nonneg, ENNReal.ofReal_coe_nnreal]

Equality of Closed Balls via Standard and Extended Distance for Nonnegative Reals

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any nonnegative real number $\varepsilon \in \mathbb{R}_{\geq 0}$, the closed ball defined using the extended distance function coincides with the closed ball defined using the standard distance function. That is: \[ \text{EMetric.closedBall}(x, \varepsilon) = \text{closedBall}(x, \varepsilon) \]

Metric.emetric_ball_top theorem

(x : α) : EMetric.ball x ⊤ = univ

Full source

@[simp]
theorem Metric.emetric_ball_top (x : α) : EMetric.ball x ⊤ = univ :=
  eq_univ_of_forall fun _ => edist_lt_top _ _

Extended Metric Ball with Infinite Radius Equals Universal Set

Informal description

For any point $x$ in a pseudometric space $\alpha$, the extended metric ball centered at $x$ with radius $\infty$ is equal to the entire space $\alpha$, i.e., $\text{EMetric.ball}(x, \infty) = \text{univ}$.

PseudoMetricSpace.replaceUniformity abbrev

 {α} [U : UniformSpace α] (m : PseudoMetricSpace α) (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) :
  PseudoMetricSpace α

Full source

/-- Build a new pseudometric space from an old one where the bundled uniform structure is provably
(but typically non-definitionaly) equal to some given uniform structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
-/
abbrev PseudoMetricSpace.replaceUniformity {α} [U : UniformSpace α] (m : PseudoMetricSpace α)
    (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : PseudoMetricSpace α :=
  { m with
    toUniformSpace := U
    uniformity_dist := H.trans PseudoMetricSpace.uniformity_dist }

Construction of Pseudometric Space from Uniformity Compatibility

Informal description

Given a uniform space $\alpha$ with uniform structure $U$ and a pseudometric space structure $m$ on $\alpha$, if the uniformity filter $\mathfrak{U}(U)$ coincides with the uniformity induced by the pseudometric space $m$, then there exists a pseudometric space structure on $\alpha$ that is compatible with $U$.

PseudoMetricSpace.replaceUniformity_eq theorem

 {α} [U : UniformSpace α] (m : PseudoMetricSpace α) (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) :
  m.replaceUniformity H = m

Full source

theorem PseudoMetricSpace.replaceUniformity_eq {α} [U : UniformSpace α] (m : PseudoMetricSpace α)
    (H : 𝓤[U] = 𝓤[PseudoEMetricSpace.toUniformSpace]) : m.replaceUniformity H = m := by
  ext
  rfl

Invariance of Pseudometric Space under Uniformity Replacement

Informal description

Let $\alpha$ be a uniform space with uniform structure $U$, and let $m$ be a pseudometric space structure on $\alpha$. If the uniformity filter $\mathfrak{U}(U)$ coincides with the uniformity induced by the pseudometric space $m$, then the pseudometric space obtained by replacing the uniformity of $m$ with $H$ is equal to $m$ itself.

PseudoMetricSpace.replaceTopology abbrev

 {γ} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ) (H : U = m.toUniformSpace.toTopologicalSpace) :
  PseudoMetricSpace γ

Full source

/-- Build a new pseudo metric space from an old one where the bundled topological structure is
provably (but typically non-definitionaly) equal to some given topological structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
-/
abbrev PseudoMetricSpace.replaceTopology {γ} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ)
    (H : U = m.toUniformSpace.toTopologicalSpace) : PseudoMetricSpace γ :=
  @PseudoMetricSpace.replaceUniformity γ (m.toUniformSpace.replaceTopology H) m rfl

Pseudometric Space Construction via Topology Compatibility

Informal description

Given a topological space $\gamma$ with topology $U$ and a pseudometric space structure $m$ on $\gamma$, if $U$ coincides with the topology induced by the uniform structure of $m$, then there exists a pseudometric space structure on $\gamma$ that is compatible with $U$.

PseudoMetricSpace.replaceTopology_eq theorem

 {γ} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ) (H : U = m.toUniformSpace.toTopologicalSpace) :
  m.replaceTopology H = m

Full source

theorem PseudoMetricSpace.replaceTopology_eq {γ} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ)
    (H : U = m.toUniformSpace.toTopologicalSpace) : m.replaceTopology H = m := by
  ext
  rfl

Pseudometric Space Topology Replacement Identity

Informal description

Let $\gamma$ be a topological space with topology $U$, and let $m$ be a pseudometric space structure on $\gamma$. If $U$ is equal to the topology induced by the uniform structure of $m$, then the pseudometric space obtained by replacing the topology of $m$ with $U$ is identical to $m$.

PseudoEMetricSpace.toPseudoMetricSpaceOfDist abbrev

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

Full source

/-- One gets a pseudometric space from an emetric space if the edistance
is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
uniformity are defeq in the pseudometric space and the pseudoemetric space. In this definition, the
distance is given separately, to be able to prescribe some expression which is not defeq to the
push-forward of the edistance to reals. See note [reducible non-instances]. -/
abbrev PseudoEMetricSpace.toPseudoMetricSpaceOfDist {α : Type u} [e : PseudoEMetricSpace α]
    (dist : α → α → ℝ) (edist_ne_top : ∀ x y : α, edistedist x y ≠ ⊤)
    (h : ∀ x y, dist x y = ENNReal.toReal (edist x y)) : PseudoMetricSpace α where
  dist := dist
  dist_self x := by simp [h]
  dist_comm x y := by simp [h, edist_comm]
  dist_triangle x y z := by
    simp only [h]
    exact ENNReal.toReal_le_add (edist_triangle _ _ _) (edist_ne_top _ _) (edist_ne_top _ _)
  edist := edist
  edist_dist _ _ := by simp only [h, ENNReal.ofReal_toReal (edist_ne_top _ _)]
  toUniformSpace := e.toUniformSpace
  uniformity_dist := e.uniformity_edist.trans <| by
    simpa only [ENNReal.coe_toNNReal (edist_ne_top _ _), h]
      using (Metric.uniformity_edist_aux fun x y : α => (edist x y).toNNReal).symm

Construction of Pseudometric Space from Extended Pseudometric Space via Distance Function

Informal description

Given a type $\alpha$ equipped with an extended pseudometric space structure $e$, a distance function $\mathrm{dist} : \alpha \to \alpha \to \mathbb{R}$, and the conditions: 1. The extended distance $\mathrm{edist}(x, y)$ is finite for all $x, y \in \alpha$, 2. The distance function satisfies $\mathrm{dist}(x, y) = \mathrm{edist}(x, y).\mathrm{toReal}$ for all $x, y \in \alpha$, then $\alpha$ can be endowed with a pseudometric space structure where the distance is given by $\mathrm{dist}$.

PseudoEMetricSpace.toPseudoMetricSpace abbrev

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

Full source

/-- One gets a pseudometric space from an emetric space if the edistance
is everywhere finite, by pushing the edistance to reals. We set it up so that the edist and the
uniformity are defeq in the pseudometric space and the emetric space. -/
abbrev PseudoEMetricSpace.toPseudoMetricSpace {α : Type u} [PseudoEMetricSpace α]
    (h : ∀ x y : α, edistedist x y ≠ ⊤) : PseudoMetricSpace α :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun x y => ENNReal.toReal (edist x y)) h fun _ _ =>
    rfl

Construction of Pseudometric Space from Finite-Distance Extended Pseudometric Space

Informal description

Given an extended pseudometric space $\alpha$ where the extended distance $\mathrm{edist}(x, y)$ is finite for all $x, y \in \alpha$, there exists a pseudometric space structure on $\alpha$ where the distance function is given by $\mathrm{dist}(x, y) = \mathrm{edist}(x, y).\mathrm{toReal}$.

PseudoMetricSpace.replaceBornology abbrev

 {α} [B : Bornology α] (m : PseudoMetricSpace α)
  (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) : PseudoMetricSpace α

Full source

/-- Build a new pseudometric space from an old one where the bundled bornology structure is provably
(but typically non-definitionaly) equal to some given bornology structure.
See Note [forgetful inheritance].
See Note [reducible non-instances].
-/
abbrev PseudoMetricSpace.replaceBornology {α} [B : Bornology α] (m : PseudoMetricSpace α)
    (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) :
    PseudoMetricSpace α :=
  { m with
    toBornology := B
    cobounded_sets := Set.ext <| compl_surjective.forall.2 fun s =>
        (H s).trans <| by rw [isBounded_iff, mem_setOf_eq, compl_compl] }

Construction of Pseudometric Space with Prescribed Bornology

Informal description

Given a type $\alpha$ with a bornology structure $B$ and a pseudometric space structure $m$ on $\alpha$, if for every subset $s \subseteq \alpha$ the boundedness with respect to $B$ is equivalent to the boundedness with respect to the bornology induced by $m$, then one can construct a new pseudometric space structure on $\alpha$ where the bornology is provably equal to $B$.

PseudoMetricSpace.replaceBornology_eq theorem

 {α} [m : PseudoMetricSpace α] [B : Bornology α]
  (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) :
  PseudoMetricSpace.replaceBornology _ H = m

Full source

theorem PseudoMetricSpace.replaceBornology_eq {α} [m : PseudoMetricSpace α] [B : Bornology α]
    (H : ∀ s, @IsBounded _ B s ↔ @IsBounded _ PseudoMetricSpace.toBornology s) :
    PseudoMetricSpace.replaceBornology _ H = m := by
  ext
  rfl

Equality of Pseudometric Space with Replaced Bornology

Informal description

Let $\alpha$ be a type equipped with a pseudometric space structure $m$ and a bornology structure $B$. If for every subset $s \subseteq \alpha$, the boundedness of $s$ with respect to $B$ is equivalent to its boundedness with respect to the bornology induced by $m$, then the pseudometric space structure obtained by replacing the bornology of $m$ with $B$ is equal to $m$ itself.

Real.pseudoMetricSpace instance

: PseudoMetricSpace ℝ

Full source

/-- Instantiate the reals as a pseudometric space. -/
instance Real.pseudoMetricSpace : PseudoMetricSpace ℝ where
  dist x y := |x - y|
  dist_self := by simp [abs_zero]
  dist_comm _ _ := abs_sub_comm _ _
  dist_triangle _ _ _ := abs_sub_le _ _ _

The Pseudometric Space Structure on Real Numbers

Informal description

The real numbers $\mathbb{R}$ 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}$.

Real.dist_eq theorem

(x y : ℝ) : dist x y = |x - y|

Full source

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

Distance Formula for Real Numbers: $\text{dist}(x, y) = |x - y|$

Informal description

For any real numbers $x$ and $y$, the distance between $x$ and $y$ is equal to the absolute value of their difference, i.e., $\text{dist}(x, y) = |x - y|$.

Real.nndist_eq theorem

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

Full source

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

Non-negative Distance as Absolute Difference in Real Numbers

Informal description

For any real numbers $x$ and $y$, the non-negative distance between $x$ and $y$ is equal to the non-negative absolute value of their difference, i.e., $\text{nndist}(x, y) = |x - y|_{\geq 0}$.

Real.nndist_eq' theorem

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

Full source

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

Non-negative Distance as Non-negative Absolute Value of Difference

Informal description

For any real numbers $x$ and $y$, the non-negative distance between $x$ and $y$ is equal to the non-negative absolute value of $y - x$, i.e., $\text{nndist}(x, y) = \text{nnabs}(y - x)$.

Real.dist_0_eq_abs theorem

(x : ℝ) : dist x 0 = |x|

Full source

theorem Real.dist_0_eq_abs (x : ℝ) : dist x 0 = |x| := by simp [Real.dist_eq]

Distance to Zero Equals Absolute Value in Real Numbers

Informal description

For any real number $x$, the distance between $x$ and $0$ equals the absolute value of $x$, i.e., $\text{dist}(x, 0) = |x|$.

Real.sub_le_dist theorem

(x y : ℝ) : x - y ≤ dist x y

Full source

theorem Real.sub_le_dist (x y : ℝ) : x - y ≤ dist x y := by
  rw [Real.dist_eq, le_abs]
  exact Or.inl (le_refl _)

Difference Bound by Distance in Real Numbers

Informal description

For any real numbers $x$ and $y$, the difference $x - y$ is less than or equal to the distance between $x$ and $y$, i.e., $x - y \leq \text{dist}(x, y)$.

Real.ball_eq_Ioo theorem

(x r : ℝ) : ball x r = Ioo (x - r) (x + r)

Full source

theorem Real.ball_eq_Ioo (x r : ℝ) : ball x r = Ioo (x - r) (x + r) :=
  Set.ext fun y => by
    rw [mem_ball, dist_comm, Real.dist_eq, abs_sub_lt_iff, mem_Ioo, ← sub_lt_iff_lt_add',
      sub_lt_comm]

Open Ball Equals Open Interval in Real Numbers: $\text{ball}(x, r) = (x - r, x + r)$

Informal description

For any real number $x$ and positive real number $r$, the open ball $\text{ball}(x, r)$ in the pseudometric space of real numbers is equal to the open interval $(x - r, x + r)$.

Real.closedBall_eq_Icc theorem

{x r : ℝ} : closedBall x r = Icc (x - r) (x + r)

Full source

theorem Real.closedBall_eq_Icc {x r : ℝ} : closedBall x r = Icc (x - r) (x + r) := by
  ext y
  rw [mem_closedBall, dist_comm, Real.dist_eq, abs_sub_le_iff, mem_Icc, ← sub_le_iff_le_add',
    sub_le_comm]

Closed Ball in Real Numbers Equals Closed Interval: $\overline{B}(x, r) = [x - r, x + r]$

Informal description

For any real numbers $x$ and $r$, the closed ball $\overline{B}(x, r)$ in the pseudometric space of real numbers is equal to the closed interval $[x - r, x + r]$.

Real.Ioo_eq_ball theorem

(x y : ℝ) : Ioo x y = ball ((x + y) / 2) ((y - x) / 2)

Full source

theorem Real.Ioo_eq_ball (x y : ℝ) : Ioo x y = ball ((x + y) / 2) ((y - x) / 2) := by
  rw [Real.ball_eq_Ioo, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two,
    ← add_div, add_assoc, add_sub_cancel, add_self_div_two]

Open Interval as Open Ball in Real Numbers: $(x, y) = \text{ball}\left(\frac{x + y}{2}, \frac{y - x}{2}\right)$

Informal description

For any real numbers $x$ and $y$, the open interval $(x, y)$ is equal to the open ball centered at $\frac{x + y}{2}$ with radius $\frac{y - x}{2}$ in the pseudometric space of real numbers, i.e., \[ (x, y) = \text{ball}\left(\frac{x + y}{2}, \frac{y - x}{2}\right). \]

Real.Icc_eq_closedBall theorem

(x y : ℝ) : Icc x y = closedBall ((x + y) / 2) ((y - x) / 2)

Full source

theorem Real.Icc_eq_closedBall (x y : ℝ) : Icc x y = closedBall ((x + y) / 2) ((y - x) / 2) := by
  rw [Real.closedBall_eq_Icc, ← sub_div, add_comm, ← sub_add, add_sub_cancel_left, add_self_div_two,
    ← add_div, add_assoc, add_sub_cancel, add_self_div_two]

Closed Interval as Closed Ball in Real Numbers: $[x, y] = \overline{B}\left(\frac{x + y}{2}, \frac{y - x}{2}\right)$

Informal description

For any real numbers $x$ and $y$, the closed interval $[x, y]$ is equal to the closed ball centered at the midpoint $\frac{x + y}{2}$ with radius $\frac{y - x}{2}$, i.e., \[ [x, y] = \overline{B}\left(\frac{x + y}{2}, \frac{y - x}{2}\right). \]

Metric.uniformity_eq_comap_nhds_zero theorem

: 𝓤 α = comap (fun p : α × α => dist p.1 p.2) (𝓝 (0 : ℝ))

Full source

theorem Metric.uniformity_eq_comap_nhds_zero :
    𝓤 α = comap (fun p : α × α => dist p.1 p.2) (𝓝 (0 : ℝ)) := by
  ext s
  simp only [mem_uniformity_dist, (nhds_basis_ball.comap _).mem_iff]
  simp [subset_def, Real.dist_0_eq_abs]

Uniformity Filter Characterization via Distance in Pseudometric Spaces

Informal description

The uniformity filter $\mathfrak{U}(\alpha)$ of a pseudometric space $\alpha$ is equal to the preimage of the neighborhood filter of $0$ in $\mathbb{R}$ under the distance function, i.e., \[ \mathfrak{U}(\alpha) = \text{comap} \, (\lambda (x, y), \text{dist}(x, y)) \, \mathcal{N}(0). \] Here, $\text{comap}$ denotes the preimage filter construction, and $\mathcal{N}(0)$ is the neighborhood filter of $0$ in $\mathbb{R}$.

tendsto_uniformity_iff_dist_tendsto_zero theorem

{f : ι → α × α} {p : Filter ι} : Tendsto f p (𝓤 α) ↔ Tendsto (fun x => dist (f x).1 (f x).2) p (𝓝 0)

Full source

theorem tendsto_uniformity_iff_dist_tendsto_zero {f : ι → α × α} {p : Filter ι} :
    TendstoTendsto f p (𝓤 α) ↔ Tendsto (fun x => dist (f x).1 (f x).2) p (𝓝 0) := by
  rw [Metric.uniformity_eq_comap_nhds_zero, tendsto_comap_iff, Function.comp_def]

Uniform Convergence Criterion via Distance in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $\mathfrak{U}(\alpha)$ its uniformity filter. For any function $f : \iota \to \alpha \times \alpha$ and any filter $p$ on $\iota$, the following are equivalent: 1. The function $f$ tends to $\mathfrak{U}(\alpha)$ along $p$. 2. The distance between the components of $f(x)$, i.e., $\text{dist}(f(x).1, f(x).2)$, tends to $0$ along $p$. In other words, $f \to \mathfrak{U}(\alpha)$ if and only if $\text{dist}(f(x).1, f(x).2) \to 0$ as $x \to p$.

Filter.Tendsto.congr_dist theorem

 {f₁ f₂ : ι → α} {p : Filter ι} {a : α} (h₁ : Tendsto f₁ p (𝓝 a)) (h : Tendsto (fun x => dist (f₁ x) (f₂ x)) p (𝓝 0)) :
  Tendsto f₂ p (𝓝 a)

Full source

theorem Filter.Tendsto.congr_dist {f₁ f₂ : ι → α} {p : Filter ι} {a : α}
    (h₁ : Tendsto f₁ p (𝓝 a)) (h : Tendsto (fun x => dist (f₁ x) (f₂ x)) p (𝓝 0)) :
    Tendsto f₂ p (𝓝 a) :=
  h₁.congr_uniformity <| tendsto_uniformity_iff_dist_tendsto_zero.2 h

Limit Preservation under Uniformly Convergent Distance in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, and let $f_1, f_2 : \iota \to \alpha$ be functions. Given a filter $p$ on $\iota$ and a point $a \in \alpha$, if $f_1$ tends to $a$ along $p$ (i.e., $\lim_{p} f_1 = a$) and the distance $\text{dist}(f_1(x), f_2(x))$ tends to $0$ along $p$, then $f_2$ also tends to $a$ along $p$.

tendsto_iff_of_dist theorem

 {f₁ f₂ : ι → α} {p : Filter ι} {a : α} (h : Tendsto (fun x => dist (f₁ x) (f₂ x)) p (𝓝 0)) :
  Tendsto f₁ p (𝓝 a) ↔ Tendsto f₂ p (𝓝 a)

Full source

theorem tendsto_iff_of_dist {f₁ f₂ : ι → α} {p : Filter ι} {a : α}
    (h : Tendsto (fun x => dist (f₁ x) (f₂ x)) p (𝓝 0)) : TendstoTendsto f₁ p (𝓝 a) ↔ Tendsto f₂ p (𝓝 a) :=
  Uniform.tendsto_congr <| tendsto_uniformity_iff_dist_tendsto_zero.2 h

Limit Equivalence under Vanishing Distance in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $f_1, f_2 \colon \iota \to \alpha$ be two functions, $p$ a filter on $\iota$, and $a \in \alpha$. If the distance between $f_1(x)$ and $f_2(x)$ tends to $0$ along $p$, then $f_1$ tends to $a$ along $p$ if and only if $f_2$ tends to $a$ along $p$. In other words, if $\text{dist}(f_1(x), f_2(x)) \to 0$ as $x \to p$, then: \[ \lim_{x \to p} f_1(x) = a \iff \lim_{x \to p} f_2(x) = a. \]

PseudoMetricSpace.dist_eq_of_dist_zero theorem

(x : α) {y z : α} (h : dist y z = 0) : dist x y = dist x z

Full source

theorem PseudoMetricSpace.dist_eq_of_dist_zero (x : α) {y z : α} (h : dist y z = 0) :
    dist x y = dist x z :=
  dist_comm y x ▸ dist_comm z x ▸ sub_eq_zero.1 (abs_nonpos_iff.1 (h ▸ abs_dist_sub_le y z x))

Distance Equality under Zero Distance Condition in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$, and any two points $y, z \in \alpha$ such that $\text{dist}(y, z) = 0$, the distances from $x$ to $y$ and from $x$ to $z$ are equal, i.e., $\text{dist}(x, y) = \text{dist}(x, z)$.

dist_dist_dist_le_left theorem

(x y z : α) : dist (dist x z) (dist y z) ≤ dist x y

Full source

theorem dist_dist_dist_le_left (x y z : α) : dist (dist x z) (dist y z) ≤ dist x y :=
  abs_dist_sub_le ..

Distance Between Distances is Bounded by Point Distance (Left Version)

Informal description

For any three points $x, y, z$ in a pseudometric space $\alpha$, the distance between the distances from $x$ to $z$ and from $y$ to $z$ is bounded by the distance between $x$ and $y$, i.e., \[ \text{dist}(\text{dist}(x, z), \text{dist}(y, z)) \leq \text{dist}(x, y). \]

dist_dist_dist_le_right theorem

(x y z : α) : dist (dist x y) (dist x z) ≤ dist y z

Full source

theorem dist_dist_dist_le_right (x y z : α) : dist (dist x y) (dist x z) ≤ dist y z := by
  simpa only [dist_comm x] using dist_dist_dist_le_left y z x

Distance Between Distances is Bounded by Point Distance (Right Version)

Informal description

For any three points $x, y, z$ in a pseudometric space $\alpha$, the distance between the distances from $x$ to $y$ and from $x$ to $z$ is bounded by the distance between $y$ and $z$, i.e., \[ \text{dist}(\text{dist}(x, y), \text{dist}(x, z)) \leq \text{dist}(y, z). \]

dist_dist_dist_le theorem

(x y x' y' : α) : dist (dist x y) (dist x' y') ≤ dist x x' + dist y y'

Full source

theorem dist_dist_dist_le (x y x' y' : α) : dist (dist x y) (dist x' y') ≤ dist x x' + dist y y' :=
  (dist_triangle _ _ _).trans <|
    add_le_add (dist_dist_dist_le_left _ _ _) (dist_dist_dist_le_right _ _ _)

Distance Between Distances is Bounded by Sum of Point Distances

Informal description

For any four points $x, y, x', y'$ in a pseudometric space $\alpha$, the distance between the distances $\text{dist}(x, y)$ and $\text{dist}(x', y')$ is bounded by the sum of the distances $\text{dist}(x, x')$ and $\text{dist}(y, y')$, i.e., \[ \text{dist}(\text{dist}(x, y), \text{dist}(x', y')) \leq \text{dist}(x, x') + \text{dist}(y, y'). \]

nhds_comap_dist theorem

(a : α) : ((𝓝 (0 : ℝ)).comap (dist · a)) = 𝓝 a

Full source

theorem nhds_comap_dist (a : α) : ((𝓝 (0 : ℝ)).comap (dist · a)) = 𝓝 a := by
  simp only [@nhds_eq_comap_uniformity α, Metric.uniformity_eq_comap_nhds_zero, comap_comap,
    Function.comp_def, dist_comm]

Neighborhood Filter Characterization via Distance Function in Pseudometric Spaces

Informal description

For any point $a$ in a pseudometric space $\alpha$, the neighborhood filter $\mathcal{N}(a)$ is equal to the preimage of the neighborhood filter of $0$ in $\mathbb{R}$ under the function $x \mapsto \text{dist}(x, a)$. In other words, \[ \mathcal{N}(a) = \text{comap} \, (\lambda x, \text{dist}(x, a)) \, \mathcal{N}(0). \]

tendsto_iff_dist_tendsto_zero theorem

{f : β → α} {x : Filter β} {a : α} : Tendsto f x (𝓝 a) ↔ Tendsto (fun b => dist (f b) a) x (𝓝 0)

Full source

theorem tendsto_iff_dist_tendsto_zero {f : β → α} {x : Filter β} {a : α} :
    TendstoTendsto f x (𝓝 a) ↔ Tendsto (fun b => dist (f b) a) x (𝓝 0) := by
  rw [← nhds_comap_dist a, tendsto_comap_iff, Function.comp_def]

Characterization of Limit via Distance Tending to Zero in Pseudometric Spaces

Informal description

For a function $f \colon \beta \to \alpha$ from a type $\beta$ to a pseudometric space $\alpha$, a filter $x$ on $\beta$, and a point $a \in \alpha$, the function $f$ tends to $a$ along the filter $x$ if and only if the distance between $f(b)$ and $a$ tends to $0$ along $x$. In other words, \[ \lim_{x} f = a \quad \text{if and only if} \quad \lim_{x} \text{dist}(f(b), a) = 0. \]

Metric.ball_subset_interior_closedBall theorem

: ball x ε ⊆ interior (closedBall x ε)

Full source

theorem ball_subset_interior_closedBall : ballball x ε ⊆ interior (closedBall x ε) :=
  interior_maximal ball_subset_closedBall isOpen_ball

Open Ball is Contained in Interior of Closed Ball in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon$, the open ball $B(x, \varepsilon)$ is contained in the interior of the closed ball $\overline{B}(x, \varepsilon)$. That is, $B(x, \varepsilon) \subseteq \text{interior}(\overline{B}(x, \varepsilon))$.

Metric.mem_closure_iff theorem

{s : Set α} {a : α} : a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

Full source

/-- ε-characterization of the closure in pseudometric spaces -/
theorem mem_closure_iff {s : Set α} {a : α} : a ∈ closure sa ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε :=
  (mem_closure_iff_nhds_basis nhds_basis_ball).trans <| by simp only [mem_ball, dist_comm]

$\varepsilon$-Characterization of Closure in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $s \subseteq \alpha$ a subset, and $a \in \alpha$. Then $a$ belongs to the closure of $s$ if and only if for every $\varepsilon > 0$, there exists $b \in s$ such that the distance between $a$ and $b$ is less than $\varepsilon$, i.e., $\text{dist}(a, b) < \varepsilon$.

Metric.mem_closure_range_iff theorem

{e : β → α} {a : α} : a ∈ closure (range e) ↔ ∀ ε > 0, ∃ k : β, dist a (e k) < ε

Full source

theorem mem_closure_range_iff {e : β → α} {a : α} :
    a ∈ closure (range e)a ∈ closure (range e) ↔ ∀ ε > 0, ∃ k : β, dist a (e k) < ε := by
  simp only [mem_closure_iff, exists_range_iff]

Characterization of Closure of Function Range in Pseudometric Spaces

Informal description

Let $e : \beta \to \alpha$ be a function from a type $\beta$ to a pseudometric space $\alpha$, and let $a \in \alpha$. Then $a$ belongs to the closure of the range of $e$ if and only if for every $\varepsilon > 0$, there exists $k \in \beta$ such that the distance between $a$ and $e(k)$ is less than $\varepsilon$.

Metric.mem_closure_range_iff_nat theorem

{e : β → α} {a : α} : a ∈ closure (range e) ↔ ∀ n : ℕ, ∃ k : β, dist a (e k) < 1 / ((n : ℝ) + 1)

Full source

theorem mem_closure_range_iff_nat {e : β → α} {a : α} :
    a ∈ closure (range e)a ∈ closure (range e) ↔ ∀ n : ℕ, ∃ k : β, dist a (e k) < 1 / ((n : ℝ) + 1) :=
  (mem_closure_iff_nhds_basis nhds_basis_ball_inv_nat_succ).trans <| by
    simp only [mem_ball, dist_comm, exists_range_iff, forall_const]

Closure of Function Range via Reciprocal Distance Condition in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space, $e : \beta \to \alpha$ a function, and $a \in \alpha$. Then $a$ belongs to the closure of the range of $e$ if and only if for every natural number $n$, there exists $k \in \beta$ such that the distance between $a$ and $e(k)$ is less than $\frac{1}{n+1}$.

Metric.mem_of_closed' theorem

{s : Set α} (hs : IsClosed s) {a : α} : a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

Full source

theorem mem_of_closed' {s : Set α} (hs : IsClosed s) {a : α} :
    a ∈ sa ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε := by
  simpa only [hs.closure_eq] using @mem_closure_iff _ _ s a

$\varepsilon$-Characterization of Membership in Closed Sets in Pseudometric Spaces

Informal description

Let $\alpha$ be a pseudometric space and $s \subseteq \alpha$ a closed subset. Then a point $a \in \alpha$ belongs to $s$ if and only if for every $\varepsilon > 0$, there exists a point $b \in s$ such that the distance between $a$ and $b$ is less than $\varepsilon$, i.e., $\text{dist}(a, b) < \varepsilon$.

Metric.dense_iff theorem

{s : Set α} : Dense s ↔ ∀ x, ∀ r > 0, (ball x r ∩ s).Nonempty

Full source

theorem dense_iff {s : Set α} : DenseDense s ↔ ∀ x, ∀ r > 0, (ball x r ∩ s).Nonempty :=
  forall_congr' fun x => by
    simp only [mem_closure_iff, Set.Nonempty, exists_prop, mem_inter_iff, mem_ball', and_comm]

Characterization of Dense Subsets via Nonempty Intersection with Balls

Informal description

A subset $s$ of a pseudometric space $\alpha$ is dense if and only if for every point $x \in \alpha$ and every positive real number $r > 0$, the intersection of the open ball $\text{ball}(x, r)$ with $s$ is nonempty.

Metric.dense_iff_iUnion_ball theorem

(s : Set α) : Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ

Full source

theorem dense_iff_iUnion_ball (s : Set α) : DenseDense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ := by
  simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff,
    forall_comm (α := α)]

Characterization of Dense Subsets via Union of Balls in Pseudometric Spaces

Informal description

A subset $s$ of a pseudometric space $\alpha$ is dense if and only if for every positive real number $r > 0$, the union of open balls of radius $r$ centered at points in $s$ equals the entire space $\alpha$, i.e., $\bigcup_{c \in s} \text{ball}(c, r) = \text{univ}$.

Metric.denseRange_iff theorem

{f : β → α} : DenseRange f ↔ ∀ x, ∀ r > 0, ∃ y, dist x (f y) < r

Full source

theorem denseRange_iff {f : β → α} : DenseRangeDenseRange f ↔ ∀ x, ∀ r > 0, ∃ y, dist x (f y) < r :=
  forall_congr' fun x => by simp only [mem_closure_iff, exists_range_iff]

Characterization of Dense Range in Pseudometric Spaces

Informal description

A function $f \colon \beta \to \alpha$ has dense range in a pseudometric space $\alpha$ if and only if for every point $x \in \alpha$ and every positive real number $r > 0$, there exists an element $y \in \beta$ such that the distance between $x$ and $f(y)$ is less than $r$, i.e., $\text{dist}(x, f(y)) < r$.

instPseudoMetricSpaceAdditive instance

: PseudoMetricSpace (Additive α)

Full source

instance : PseudoMetricSpace (Additive α) := ‹_›

Pseudometric Space Structure on Additive Types

Informal description

For any pseudometric space $\alpha$, the additive version $\text{Additive}\,\alpha$ inherits a pseudometric space structure where the distance function is preserved.

instPseudoMetricSpaceMultiplicative instance

: PseudoMetricSpace (Multiplicative α)

Full source

instance : PseudoMetricSpace (Multiplicative α) := ‹_›

Pseudometric Space Structure on Multiplicative Groups

Informal description

For any pseudometric space $\alpha$, the multiplicative group structure on $\alpha$ inherits a pseudometric space structure where the distance function is preserved.

nndist_ofMul theorem

(a b : X) : nndist (ofMul a) (ofMul b) = nndist a b

Full source

@[simp] theorem nndist_ofMul (a b : X) : nndist (ofMul a) (ofMul b) = nndist a b := rfl

Preservation of Non-Negative Distance under `ofMul`

Informal description

For any two elements $a$ and $b$ in a pseudometric space $X$, the non-negative distance between their images under the `ofMul` function is equal to the non-negative distance between $a$ and $b$ themselves, i.e., $\text{nndist}(\text{ofMul}(a), \text{ofMul}(b)) = \text{nndist}(a, b)$.

nndist_ofAdd theorem

(a b : X) : nndist (ofAdd a) (ofAdd b) = nndist a b

Full source

@[simp] theorem nndist_ofAdd (a b : X) : nndist (ofAdd a) (ofAdd b) = nndist a b := rfl

Preservation of Non-Negative Distance under `ofAdd` Mapping

Informal description

For any two elements $a$ and $b$ in a pseudometric space $X$, the non-negative distance between their images under the `ofAdd` function is equal to the non-negative distance between $a$ and $b$ themselves, i.e., $\text{nndist}(\text{ofAdd}(a), \text{ofAdd}(b)) = \text{nndist}(a, b)$.

nndist_toMul theorem

(a b : Additive X) : nndist a.toMul b.toMul = nndist a b

Full source

@[simp] theorem nndist_toMul (a b : Additive X) : nndist a.toMul b.toMul = nndist a b := rfl

Preservation of Non-Negative Distance under Multiplicative Conversion

Informal description

For any two elements $a$ and $b$ in the additive version of a pseudometric space $X$, the non-negative distance between their multiplicative counterparts equals the non-negative distance between $a$ and $b$, i.e., $\text{nndist}(a.\text{toMul}, b.\text{toMul}) = \text{nndist}(a, b)$.

nndist_toAdd theorem

(a b : Multiplicative X) : nndist a.toAdd b.toAdd = nndist a b

Full source

@[simp]
theorem nndist_toAdd (a b : Multiplicative X) : nndist a.toAdd b.toAdd = nndist a b := rfl

Preservation of Non-Negative Distance under Multiplicative-to-Additive Conversion

Informal description

For any elements $a$ and $b$ in the multiplicative group $\text{Multiplicative } X$, the non-negative distance between their images under the $\text{toAdd}$ map equals the non-negative distance between $a$ and $b$ themselves, i.e., $\text{nndist}(\text{toAdd}(a), \text{toAdd}(b)) = \text{nndist}(a, b)$.

instPseudoMetricSpaceOrderDual instance

: PseudoMetricSpace αᵒᵈ

Full source

instance : PseudoMetricSpace αᵒᵈ := ‹_›

Pseudometric Space Structure on Order Duals

Informal description

For any pseudometric space $\alpha$, the order dual $\alpha^{\text{op}}$ is also a pseudometric space with the same distance function.

nndist_toDual theorem

(a b : X) : nndist (toDual a) (toDual b) = nndist a b

Full source

@[simp] theorem nndist_toDual (a b : X) : nndist (toDual a) (toDual b) = nndist a b := rfl

Non-negative Distance Preservation under Order Duality

Informal description

For any two elements $a$ and $b$ in a pseudometric space $X$, the non-negative distance between their order duals is equal to the non-negative distance between $a$ and $b$, i.e., $\text{nndist}(\text{toDual}(a), \text{toDual}(b)) = \text{nndist}(a, b)$.

nndist_ofDual theorem

(a b : Xᵒᵈ) : nndist (ofDual a) (ofDual b) = nndist a b

Full source

@[simp] theorem nndist_ofDual (a b : Xᵒᵈ) : nndist (ofDual a) (ofDual b) = nndist a b := rfl

Preservation of Non-Negative Distance under Order Dual Map

Informal description

For any two elements $a$ and $b$ in the order dual $X^{\text{op}}$ of a pseudometric space $X$, the non-negative distance between their images under the `ofDual` map equals the non-negative distance between $a$ and $b$ in $X^{\text{op}}$, i.e., $\text{nndist}(\text{ofDual}(a), \text{ofDual}(b)) = \text{nndist}(a, b)$.

Mathlib.Topology.MetricSpace.Pseudo.Defs

Main definitions

Tags