## Pseudo-metric spaces #

This file defines pseudo-metric spaces: these differ from metric spaces by not imposing the condition `dist x y = 0 → x = y`. Many definitions and theorems expected on (pseudo-)metric spaces are already introduced on uniform spaces and topological spaces. For example: open and closed sets, compactness, completeness, continuity and uniform continuity.

## Main definitions #

- `Dist α`: Endows a space `α` with a function `dist a b`.
- `PseudoMetricSpace α`: A space endowed with a distance function, which can be zero even if the two elements are non-equal.
- `Metric.ball x ε`: The set of all points `y` with `dist y x < ε`.
- `Metric.Bounded s`: Whether a subset of a `PseudoMetricSpace` is bounded.
- `MetricSpace α`: A `PseudoMetricSpace` with the guarantee `dist x y = 0 → x = y`.

Additional useful definitions:

- `nndist a b`: `dist` as a function to the non-negative reals.
- `Metric.closedBall x ε`: The set of all points `y` with `dist y x ≤ ε`.
- `Metric.sphere x ε`: The set of all points `y` with `dist y x = ε`.

TODO (anyone): Add "Main results" section.

## Tags #

pseudo_metric, dist

source
theorem UniformSpace.ofDist_aux (ε : ℝ) (hε : 0 < ε) :
∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
source
def UniformSpace.ofDist {α : Type u} (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 α

Construct a uniform structure from a distance function and metric space axioms

Equations

- UniformSpace.ofDist dist dist_self dist_comm dist_triangle = UniformSpace.ofFun dist dist_self dist_comm dist_triangle UniformSpace.ofDist_aux

Instances For

source
@[reducible, inline]
abbrev Bornology.ofDist {α : Type u_3} (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 α

Construct a bornology from a distance function and metric space axioms.

Equations

- Bornology.ofDist dist dist_comm dist_triangle = Bornology.ofBounded {s : Set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C} ⋯ ⋯ ⋯ ⋯

Instances For

source
class Dist (α : Type u_3) :
Type u_3

The distance function (given an ambient metric space on `α`), which returns a nonnegative real number `dist x y` given `x y : α`.

- dist : α → α → ℝ

  Distance between two points

Instances

source
theorem Dist.ext_iff {α : Type u_3} {x y : Dist α} :
x = y ↔ dist = dist
source
theorem Dist.ext {α : Type u_3} {x y : Dist α} (dist : dist = dist) :
x = y
source
class PseudoMetricSpace (α : Type u) extends Dist α :
Type u

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 e.g. 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].

- 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
- edist : α → α → ENNReal

  Extended distance between two points

- edist_dist (x y : α) : edist x y = ENNReal.ofReal (dist x y)
- toUniformSpace : UniformSpace α
- uniformity_dist : uniformity α = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | dist p.1 p.2 < ε}
- toBornology : Bornology α
- cobounded_sets : (Bornology.cobounded α).sets = {s : Set α | ∃ (C : ℝ), ∀ x ∈ s ᶜ, ∀ y ∈ s ᶜ, dist x y ≤ C}

Instances

source
theorem PseudoMetricSpace.ext {α : Type u_3} {m m' : PseudoMetricSpace α} (h : m.toDist = m'.toDist) :
m = m'

Two pseudo metric space structures with the same distance function coincide.

source
theorem PseudoMetricSpace.ext_iff {α : Type u_3} {m m' : PseudoMetricSpace α} :
m = m' ↔ m.toDist = m'.toDist
source
@[instance 200]
instance PseudoMetricSpace.toEDist {α : Type u} [PseudoMetricSpace α] :
EDist α
Equations

- PseudoMetricSpace.toEDist = { edist := PseudoMetricSpace.edist }

source
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 α), IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : α), dist x y < ε → y ∈ s) :
PseudoMetricSpace α

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.

Equations

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

Instances For

source
@[simp]
theorem dist_self {α : Type u} [PseudoMetricSpace α] (x : α) :
dist x x = 0
source
theorem dist_comm {α : Type u} [PseudoMetricSpace α] (x y : α) :
dist x y = dist y x
source
theorem edist_dist {α : Type u} [PseudoMetricSpace α] (x y : α) :
edist x y = ENNReal.ofReal (dist x y)
source
theorem dist_triangle {α : Type u} [PseudoMetricSpace α] (x y z : α) :
dist x z ≤ dist x y + dist y z
source
theorem dist_triangle_left {α : Type u} [PseudoMetricSpace α] (x y z : α) :
dist x y ≤ dist z x + dist z y
source
theorem dist_triangle_right {α : Type u} [PseudoMetricSpace α] (x y z : α) :
dist x y ≤ dist x z + dist y z
source
theorem dist_triangle4 {α : Type u} [PseudoMetricSpace α] (x y z w : α) :
dist x w ≤ dist x y + dist y z + dist z w
source
theorem dist_triangle4_left {α : Type u} [PseudoMetricSpace α] (x₁ y₁ x₂ y₂ : α) :
dist x₂ y₂ ≤ dist x₁ y₁ + (dist x₁ x₂ + dist y₁ y₂)
source
theorem dist_triangle4_right {α : Type u} [PseudoMetricSpace α] (x₁ y₁ x₂ y₂ : α) :
dist x₁ y₁ ≤ dist x₁ x₂ + dist y₁ y₂ + dist x₂ y₂
source
theorem dist_triangle8 {α : Type u} [PseudoMetricSpace α] (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
source
theorem swap_dist {α : Type u} [PseudoMetricSpace α] :
Function.swap dist = dist
source
theorem abs_dist_sub_le {α : Type u} [PseudoMetricSpace α] (x y z : α) :
|dist x z - dist y z| ≤ dist x y
source
@[simp]
theorem dist_nonneg {α : Type u} [PseudoMetricSpace α] {x y : α} :
0 ≤ dist x y
source
def Mathlib.Meta.Positivity.evalDist :
PositivityExt

Extension for the `positivity` tactic: distances are nonnegative.

Instances For

source
@[simp]
theorem abs_dist {α : Type u} [PseudoMetricSpace α] {a b : α} :
|dist a b| = dist a b
source
class NNDist (α : Type u_3) :
Type u_3

A version of `Dist` that takes value in `ℝ≥0`.

- nndist : α → α → NNReal

  Nonnegative distance between two points

Instances

source
@[instance 100]
instance PseudoMetricSpace.toNNDist {α : Type u} [PseudoMetricSpace α] :
NNDist α

Distance as a nonnegative real number.

Equations

- PseudoMetricSpace.toNNDist = { nndist := fun (a b : α) => ⟨dist a b, ⋯⟩ }

source
theorem dist_nndist {α : Type u} [PseudoMetricSpace α] (x y : α) :
dist x y = ↑(nndist x y)

Express `dist` in terms of `nndist`

source
@[simp]
theorem coe_nndist {α : Type u} [PseudoMetricSpace α] (x y : α) :
↑(nndist x y) = dist x y
source
theorem edist_nndist {α : Type u} [PseudoMetricSpace α] (x y : α) :
edist x y = ↑(nndist x y)

Express `edist` in terms of `nndist`

source
theorem nndist_edist {α : Type u} [PseudoMetricSpace α] (x y : α) :
nndist x y = (edist x y).toNNReal

Express `nndist` in terms of `edist`

source
@[simp]
theorem coe_nnreal_ennreal_nndist {α : Type u} [PseudoMetricSpace α] (x y : α) :
↑(nndist x y) = edist x y
source
@[simp]
theorem edist_lt_coe {α : Type u} [PseudoMetricSpace α] {x y : α} {c : NNReal} :
edist x y < ↑c ↔ nndist x y < c
source
@[simp]
theorem edist_le_coe {α : Type u} [PseudoMetricSpace α] {x y : α} {c : NNReal} :
edist x y ≤ ↑c ↔ nndist x y ≤ c
source
theorem edist_lt_top {α : Type u_3} [PseudoMetricSpace α] (x y : α) :
edist x y < ⊤

In a pseudometric space, the extended distance is always finite

source
theorem edist_ne_top {α : Type u} [PseudoMetricSpace α] (x y : α) :
edist x y ≠ ⊤

In a pseudometric space, the extended distance is always finite

source
@[simp]
theorem nndist_self {α : Type u} [PseudoMetricSpace α] (a : α) :
nndist a a = 0

`nndist x x` vanishes

source
@[simp]
theorem dist_lt_coe {α : Type u} [PseudoMetricSpace α] {x y : α} {c : NNReal} :
dist x y < ↑c ↔ nndist x y < c
source
@[simp]
theorem dist_le_coe {α : Type u} [PseudoMetricSpace α] {x y : α} {c : NNReal} :
dist x y ≤ ↑c ↔ nndist x y ≤ c
source
@[simp]
theorem edist_lt_ofReal {α : Type u} [PseudoMetricSpace α] {x y : α} {r : ℝ} :
edist x y < ENNReal.ofReal r ↔ dist x y < r
source
@[simp]
theorem edist_le_ofReal {α : Type u} [PseudoMetricSpace α] {x y : α} {r : ℝ} (hr : 0 ≤ r) :
edist x y ≤ ENNReal.ofReal r ↔ dist x y ≤ r
source
theorem nndist_dist {α : Type u} [PseudoMetricSpace α] (x y : α) :
nndist x y = (dist x y).toNNReal

Express `nndist` in terms of `dist`

source
theorem nndist_comm {α : Type u} [PseudoMetricSpace α] (x y : α) :
nndist x y = nndist y x
source
theorem nndist_triangle {α : Type u} [PseudoMetricSpace α] (x y z : α) :
nndist x z ≤ nndist x y + nndist y z

Triangle inequality for the nonnegative distance

source
theorem nndist_triangle_left {α : Type u} [PseudoMetricSpace α] (x y z : α) :
nndist x y ≤ nndist z x + nndist z y
source
theorem nndist_triangle_right {α : Type u} [PseudoMetricSpace α] (x y z : α) :
nndist x y ≤ nndist x z + nndist y z
source
theorem dist_edist {α : Type u} [PseudoMetricSpace α] (x y : α) :
dist x y = (edist x y).toReal

Express `dist` in terms of `edist`

source
def Metric.ball {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) :
Set α

`ball x ε` is the set of all points `y` with `dist y x < ε`

Equations

- Metric.ball x ε = {y : α | dist y x < ε}

Instances For

source
@[simp]
theorem Metric.mem_ball {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} :
y ∈ ball x ε ↔ dist y x < ε
source
theorem Metric.mem_ball' {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} :
y ∈ ball x ε ↔ dist x y < ε
source
theorem Metric.pos_of_mem_ball {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (hy : y ∈ ball x ε) :
0 < ε
source
theorem Metric.mem_ball_self {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 < ε) :
x ∈ ball x ε
source
@[simp]
theorem Metric.nonempty_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
(ball x ε).Nonempty ↔ 0 < ε
source
@[simp]
theorem Metric.ball_eq_empty {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
ball x ε = ∅ ↔ ε ≤ 0
source
@[simp]
theorem Metric.ball_zero {α : Type u} [PseudoMetricSpace α] {x : α} :
ball x 0 = ∅
source
theorem Metric.exists_lt_mem_ball_of_mem_ball {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (h : x ∈ ball y ε) :
∃ ε' < ε, x ∈ ball y ε'

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`.

source
theorem Metric.ball_eq_ball {α : Type u} [PseudoMetricSpace α] (ε : ℝ) (x : α) :
UniformSpace.ball x {p : α × α | dist p.2 p.1 < ε} = ball x ε
source
theorem Metric.ball_eq_ball' {α : Type u} [PseudoMetricSpace α] (ε : ℝ) (x : α) :
UniformSpace.ball x {p : α × α | dist p.1 p.2 < ε} = ball x ε
source
@[simp]
theorem Metric.iUnion_ball_nat {α : Type u} [PseudoMetricSpace α] (x : α) :
⋃ (n : ℕ), ball x ↑n = Set.univ
source
@[simp]
theorem Metric.iUnion_ball_nat_succ {α : Type u} [PseudoMetricSpace α] (x : α) :
⋃ (n : ℕ), ball x (↑n + 1) = Set.univ
source
def Metric.closedBall {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) :
Set α

`closedBall x ε` is the set of all points `y` with `dist y x ≤ ε`

Equations

- Metric.closedBall x ε = {y : α | dist y x ≤ ε}

Instances For

source
@[simp]
theorem Metric.mem_closedBall {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} :
y ∈ closedBall x ε ↔ dist y x ≤ ε
source
theorem Metric.mem_closedBall' {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} :
y ∈ closedBall x ε ↔ dist x y ≤ ε
source
def Metric.sphere {α : Type u} [PseudoMetricSpace α] (x : α) (ε : ℝ) :
Set α

`sphere x ε` is the set of all points `y` with `dist y x = ε`

Equations

- Metric.sphere x ε = {y : α | dist y x = ε}

Instances For

source
@[simp]
theorem Metric.mem_sphere {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} :
y ∈ sphere x ε ↔ dist y x = ε
source
theorem Metric.mem_sphere' {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} :
y ∈ sphere x ε ↔ dist x y = ε
source
theorem Metric.ne_of_mem_sphere {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (h : y ∈ sphere x ε) (hε : ε ≠ 0) :
y ≠ x
source
theorem Metric.nonneg_of_mem_sphere {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (hy : y ∈ sphere x ε) :
0 ≤ ε
source
@[simp]
theorem Metric.sphere_eq_empty_of_neg {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (hε : ε < 0) :
sphere x ε = ∅
source
theorem Metric.sphere_eq_empty_of_subsingleton {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (hε : ε ≠ 0) :
sphere x ε = ∅
source
instance Metric.sphere_isEmpty_of_subsingleton {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] [NeZero ε] :
IsEmpty ↑(sphere x ε)
source
theorem Metric.closedBall_eq_singleton_of_subsingleton {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (h : 0 ≤ ε) :
closedBall x ε = {x}
source
theorem Metric.ball_eq_singleton_of_subsingleton {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α] (h : 0 < ε) :
ball x ε = {x}
source
theorem Metric.mem_closedBall_self {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 ≤ ε) :
x ∈ closedBall x ε
source
@[simp]
theorem Metric.nonempty_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
(closedBall x ε).Nonempty ↔ 0 ≤ ε
source
@[simp]
theorem Metric.closedBall_eq_empty {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
closedBall x ε = ∅ ↔ ε < 0
source
@[simp]
theorem Metric.closedBall_of_neg {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
ε < 0 → closedBall x ε = ∅

Alias of the reverse direction of `Metric.closedBall_eq_empty`.

source
theorem Metric.closedBall_eq_sphere_of_nonpos {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (hε : ε ≤ 0) :
closedBall x ε = sphere x ε

Closed balls and spheres coincide when the radius is non-positive

source
theorem Metric.ball_subset_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
ball x ε ⊆ closedBall x ε
source
theorem Metric.sphere_subset_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
sphere x ε ⊆ closedBall x ε
source
theorem Metric.sphere_subset_ball {α : Type u} [PseudoMetricSpace α] {x : α} {r R : ℝ} (h : r < R) :
sphere x r ⊆ ball x R
source
theorem Metric.closedBall_disjoint_ball {α : Type u} [PseudoMetricSpace α] {x y : α} {δ ε : ℝ} (h : δ + ε ≤ dist x y) :
Disjoint (closedBall x δ) (ball y ε)
source
theorem Metric.ball_disjoint_closedBall {α : Type u} [PseudoMetricSpace α] {x y : α} {δ ε : ℝ} (h : δ + ε ≤ dist x y) :
Disjoint (ball x δ) (closedBall y ε)
source
theorem Metric.ball_disjoint_ball {α : Type u} [PseudoMetricSpace α] {x y : α} {δ ε : ℝ} (h : δ + ε ≤ dist x y) :
Disjoint (ball x δ) (ball y ε)
source
theorem Metric.closedBall_disjoint_closedBall {α : Type u} [PseudoMetricSpace α] {x y : α} {δ ε : ℝ} (h : δ + ε < dist x y) :
Disjoint (closedBall x δ) (closedBall y ε)
source
theorem Metric.sphere_disjoint_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
Disjoint (sphere x ε) (ball x ε)
source
@[simp]
theorem Metric.ball_union_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
ball x ε ∪ sphere x ε = closedBall x ε
source
@[simp]
theorem Metric.sphere_union_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
sphere x ε ∪ ball x ε = closedBall x ε
source
@[simp]
theorem Metric.closedBall_diff_sphere {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
closedBall x ε \ sphere x ε = ball x ε
source
@[simp]
theorem Metric.closedBall_diff_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
closedBall x ε \ ball x ε = sphere x ε
source
theorem Metric.mem_ball_comm {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} :
x ∈ ball y ε ↔ y ∈ ball x ε
source
theorem Metric.mem_closedBall_comm {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} :
x ∈ closedBall y ε ↔ y ∈ closedBall x ε
source
theorem Metric.mem_sphere_comm {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} :
x ∈ sphere y ε ↔ y ∈ sphere x ε
source
theorem Metric.ball_subset_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ ≤ ε₂) :
ball x ε₁ ⊆ ball x ε₂
source
theorem Metric.closedBall_eq_bInter_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
closedBall x ε = ⋂ (δ : ℝ), ⋂ (_ : δ > ε), ball x δ
source
theorem Metric.ball_subset_ball' {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y ≤ ε₂) :
ball x ε₁ ⊆ ball y ε₂
source
theorem Metric.closedBall_subset_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ ≤ ε₂) :
closedBall x ε₁ ⊆ closedBall x ε₂
source
theorem Metric.closedBall_subset_closedBall' {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y ≤ ε₂) :
closedBall x ε₁ ⊆ closedBall y ε₂
source
theorem Metric.closedBall_subset_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε₁ ε₂ : ℝ} (h : ε₁ < ε₂) :
closedBall x ε₁ ⊆ ball x ε₂
source
theorem Metric.closedBall_subset_ball' {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : ε₁ + dist x y < ε₂) :
closedBall x ε₁ ⊆ ball y ε₂
source
theorem Metric.dist_le_add_of_nonempty_closedBall_inter_closedBall {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (closedBall x ε₁ ∩ closedBall y ε₂).Nonempty) :
dist x y ≤ ε₁ + ε₂
source
theorem Metric.dist_lt_add_of_nonempty_closedBall_inter_ball {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (closedBall x ε₁ ∩ ball y ε₂).Nonempty) :
dist x y < ε₁ + ε₂
source
theorem Metric.dist_lt_add_of_nonempty_ball_inter_closedBall {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (ball x ε₁ ∩ closedBall y ε₂).Nonempty) :
dist x y < ε₁ + ε₂
source
theorem Metric.dist_lt_add_of_nonempty_ball_inter_ball {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : (ball x ε₁ ∩ ball y ε₂).Nonempty) :
dist x y < ε₁ + ε₂
source
@[simp]
theorem Metric.iUnion_closedBall_nat {α : Type u} [PseudoMetricSpace α] (x : α) :
⋃ (n : ℕ), closedBall x ↑n = Set.univ
source
theorem Metric.iUnion_inter_closedBall_nat {α : Type u} [PseudoMetricSpace α] (s : Set α) (x : α) :
⋃ (n : ℕ), s ∩ closedBall x ↑n = s
source
theorem Metric.ball_subset {α : Type u} [PseudoMetricSpace α] {x y : α} {ε₁ ε₂ : ℝ} (h : dist x y ≤ ε₂ - ε₁) :
ball x ε₁ ⊆ ball y ε₂
source
theorem Metric.ball_half_subset {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (y : α) (h : y ∈ ball x (ε / 2)) :
ball y (ε / 2) ⊆ ball x ε
source
theorem Metric.exists_ball_subset_ball {α : Type u} [PseudoMetricSpace α] {x y : α} {ε : ℝ} (h : y ∈ ball x ε) :
∃ ε' > 0, ball y ε' ⊆ ball x ε
source
theorem Metric.forall_of_forall_mem_closedBall {α : Type u} [PseudoMetricSpace α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ closedBall x R, p y) (y : α) :
p y

If a property holds for all points in closed balls of arbitrarily large radii, then it holds for all points.

source
theorem Metric.forall_of_forall_mem_ball {α : Type u} [PseudoMetricSpace α] (p : α → Prop) (x : α) (H : ∃ᶠ (R : ℝ) in Filter.atTop, ∀ y ∈ ball x R, p y) (y : α) :
p y

If a property holds for all points in balls of arbitrarily large radii, then it holds for all points.

source
theorem Metric.isBounded_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} :
Bornology.IsBounded s ↔ ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
source
theorem Metric.boundedSpace_iff {α : Type u} [PseudoMetricSpace α] :
BoundedSpace α ↔ ∃ (C : ℝ), ∀ (a b : α), dist a b ≤ C
source
theorem Metric.isBounded_iff_eventually {α : Type u} [PseudoMetricSpace α] {s : Set α} :
Bornology.IsBounded s ↔ ∀ᶠ (C : ℝ) in Filter.atTop, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
source
theorem Metric.isBounded_iff_exists_ge {α : Type u} [PseudoMetricSpace α] {s : Set α} (c : ℝ) :
Bornology.IsBounded s ↔ ∃ (C : ℝ), c ≤ C ∧ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C
source
theorem Metric.isBounded_iff_nndist {α : Type u} [PseudoMetricSpace α] {s : Set α} :
Bornology.IsBounded s ↔ ∃ (C : NNReal), ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → nndist x y ≤ C
source
theorem Metric.boundedSpace_iff_nndist {α : Type u} [PseudoMetricSpace α] :
BoundedSpace α ↔ ∃ (C : NNReal), ∀ (a b : α), nndist a b ≤ C
source
theorem Metric.boundedSpace_iff_edist {α : Type u} [PseudoMetricSpace α] :
BoundedSpace α ↔ ∃ (C : NNReal), ∀ (a b : α), edist a b ≤ ↑C
source
theorem Metric.toUniformSpace_eq {α : Type u} [PseudoMetricSpace α] :
PseudoMetricSpace.toUniformSpace = UniformSpace.ofDist dist ⋯ ⋯ ⋯
source
theorem Metric.uniformity_basis_dist {α : Type u} [PseudoMetricSpace α] :
(uniformity α).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => {p : α × α | dist p.1 p.2 < ε}
source
theorem Metric.mk_uniformity_basis {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ} (hf₀ : ∀ (i : β), p i → 0 < f i) (hf : ∀ ⦃ε : ℝ⦄, 0 < ε → ∃ (i : β), p i ∧ f i ≤ ε) :
(uniformity α).HasBasis p fun (i : β) => {p : α × α | dist p.1 p.2 < f i}

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`.

source
theorem Metric.uniformity_basis_dist_rat {α : Type u} [PseudoMetricSpace α] :
(uniformity α).HasBasis (fun (r : ℚ) => 0 < r) fun (r : ℚ) => {p : α × α | dist p.1 p.2 < ↑r}
source
theorem Metric.uniformity_basis_dist_inv_nat_succ {α : Type u} [PseudoMetricSpace α] :
(uniformity α).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {p : α × α | dist p.1 p.2 < 1 / (↑n + 1)}
source
theorem Metric.uniformity_basis_dist_inv_nat_pos {α : Type u} [PseudoMetricSpace α] :
(uniformity α).HasBasis (fun (n : ℕ) => 0 < n) fun (n : ℕ) => {p : α × α | dist p.1 p.2 < 1 / ↑n}
source
theorem Metric.uniformity_basis_dist_pow {α : Type u} [PseudoMetricSpace α] {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
(uniformity α).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {p : α × α | dist p.1 p.2 < r ^ n}
source
theorem Metric.uniformity_basis_dist_lt {α : Type u} [PseudoMetricSpace α] {R : ℝ} (hR : 0 < R) :
(uniformity α).HasBasis (fun (r : ℝ) => 0 < r ∧ r < R) fun (r : ℝ) => {p : α × α | dist p.1 p.2 < r}
source
theorem Metric.mk_uniformity_basis_le {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ} (hf₀ : ∀ (x : β), p x → 0 < f x) (hf : ∀ (ε : ℝ), 0 < ε → ∃ (x : β), p x ∧ f x ≤ ε) :
(uniformity α).HasBasis p fun (x : β) => {p : α × α | dist p.1 p.2 ≤ f x}

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.

source
theorem Metric.uniformity_basis_dist_le {α : Type u} [PseudoMetricSpace α] :
(uniformity α).HasBasis (fun (x : ℝ) => 0 < x) fun (ε : ℝ) => {p : α × α | dist p.1 p.2 ≤ ε}

Constant size closed neighborhoods of the diagonal form a basis of the uniformity filter.

source
theorem Metric.uniformity_basis_dist_le_pow {α : Type u} [PseudoMetricSpace α] {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
(uniformity α).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => {p : α × α | dist p.1 p.2 ≤ r ^ n}
source
theorem Metric.mem_uniformity_dist {α : Type u} [PseudoMetricSpace α] {s : Set (α × α)} :
s ∈ uniformity α ↔ ∃ ε > 0, ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ s
source
theorem Metric.dist_mem_uniformity {α : Type u} [PseudoMetricSpace α] {ε : ℝ} (ε0 : 0 < ε) :
{p : α × α | dist p.1 p.2 < ε} ∈ uniformity α

A constant size neighborhood of the diagonal is an entourage.

source
theorem Metric.uniformContinuous_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} :
UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b < δ → dist (f a) (f b) < ε
source
theorem Metric.uniformContinuousOn_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {s : Set α} :
UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y < δ → dist (f x) (f y) < ε
source
theorem Metric.uniformContinuous_iff_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} :
UniformContinuous f ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃a b : α⦄, dist a b ≤ δ → dist (f a) (f b) ≤ ε
source
theorem Metric.uniformContinuousOn_iff_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {s : Set α} :
UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist (f x) (f y) ≤ ε
source
theorem Metric.nhds_basis_ball {α : Type u} [PseudoMetricSpace α] {x : α} :
(nhds x).HasBasis (fun (x : ℝ) => 0 < x) (ball x)
source
theorem Metric.mem_nhds_iff {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} :
s ∈ nhds x ↔ ∃ ε > 0, ball x ε ⊆ s
source
theorem Metric.eventually_nhds_iff {α : Type u} [PseudoMetricSpace α] {x : α} {p : α → Prop} :
(∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε > 0, ∀ ⦃y : α⦄, dist y x < ε → p y
source
theorem Metric.eventually_nhds_iff_ball {α : Type u} [PseudoMetricSpace α] {x : α} {p : α → Prop} :
(∀ᶠ (y : α) in nhds x, p y) ↔ ∃ ε > 0, ∀ y ∈ ball x ε, p y
source
theorem Metric.eventually_nhds_prod_iff {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : α × ι → Prop} :
(∀ᶠ (x : α × ι) in nhds x₀ ×ˢ f, p x) ↔ ∃ ε > 0, ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∀ ⦃x : α⦄, dist x x₀ < ε → ∀ ⦃i : ι⦄, pa i → p (x, i)

A version of `Filter.eventually_prod_iff` where the first filter consists of neighborhoods in a pseudo-metric space.

source
theorem Metric.eventually_prod_nhds_iff {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : Filter ι} {x₀ : α} {p : ι × α → Prop} :
(∀ᶠ (x : ι × α) in f ×ˢ nhds x₀, p x) ↔ ∃ (pa : ι → Prop), (∀ᶠ (i : ι) in f, pa i) ∧ ∃ ε > 0, ∀ ⦃i : ι⦄, pa i → ∀ ⦃x : α⦄, dist x x₀ < ε → p (i, x)

A version of `Filter.eventually_prod_iff` where the second filter consists of neighborhoods in a pseudo-metric space.

source
theorem Metric.nhds_basis_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} :
(nhds x).HasBasis (fun (ε : ℝ) => 0 < ε) (closedBall x)
source
theorem Metric.nhds_basis_ball_inv_nat_succ {α : Type u} [PseudoMetricSpace α] {x : α} :
(nhds x).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => ball x (1 / (↑n + 1))
source
theorem Metric.nhds_basis_ball_inv_nat_pos {α : Type u} [PseudoMetricSpace α] {x : α} :
(nhds x).HasBasis (fun (n : ℕ) => 0 < n) fun (n : ℕ) => ball x (1 / ↑n)
source
theorem Metric.nhds_basis_ball_pow {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
(nhds x).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => ball x (r ^ n)
source
theorem Metric.nhds_basis_closedBall_pow {α : Type u} [PseudoMetricSpace α] {x : α} {r : ℝ} (h0 : 0 < r) (h1 : r < 1) :
(nhds x).HasBasis (fun (x : ℕ) => True) fun (n : ℕ) => closedBall x (r ^ n)
source
theorem Metric.isOpen_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} :
IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ball x ε ⊆ s
source
@[simp]
theorem Metric.isOpen_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
IsOpen (ball x ε)
source
theorem Metric.ball_mem_nhds {α : Type u} [PseudoMetricSpace α] (x : α) {ε : ℝ} (ε0 : 0 < ε) :
ball x ε ∈ nhds x
source
theorem Metric.closedBall_mem_nhds {α : Type u} [PseudoMetricSpace α] (x : α) {ε : ℝ} (ε0 : 0 < ε) :
closedBall x ε ∈ nhds x
source
theorem Metric.closedBall_mem_nhds_of_mem {α : Type u} [PseudoMetricSpace α] {x c : α} {ε : ℝ} (h : x ∈ ball c ε) :
closedBall c ε ∈ nhds x
source
theorem Metric.nhdsWithin_basis_ball {α : Type u} [PseudoMetricSpace α] {x : α} {s : Set α} :
(nhdsWithin x s).HasBasis (fun (ε : ℝ) => 0 < ε) fun (ε : ℝ) => ball x ε ∩ s
source
theorem Metric.mem_nhdsWithin_iff {α : Type u} [PseudoMetricSpace α] {x : α} {s t : Set α} :
s ∈ nhdsWithin x t ↔ ∃ ε > 0, ball x ε ∩ t ⊆ s
source
theorem Metric.tendsto_nhdsWithin_nhdsWithin {α : Type u} {β : Type v} [PseudoMetricSpace α] {s : Set α} [PseudoMetricSpace β] {t : Set β} {f : α → β} {a : α} {b : β} :
Filter.Tendsto f (nhdsWithin a s) (nhdsWithin b t) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → f x ∈ t ∧ dist (f x) b < ε
source
theorem Metric.tendsto_nhdsWithin_nhds {α : Type u} {β : Type v} [PseudoMetricSpace α] {s : Set α} [PseudoMetricSpace β] {f : α → β} {a : α} {b : β} :
Filter.Tendsto f (nhdsWithin a s) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) b < ε
source
theorem Metric.tendsto_nhds_nhds {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {a : α} {b : β} :
Filter.Tendsto f (nhds a) (nhds b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) b < ε
source
theorem Metric.continuousAt_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {a : α} :
ContinuousAt f a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, dist x a < δ → dist (f x) (f a) < ε
source
theorem Metric.continuousWithinAt_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {a : α} {s : Set α} :
ContinuousWithinAt f s a ↔ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → dist x a < δ → dist (f x) (f a) < ε
source
theorem Metric.continuousOn_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {s : Set α} :
ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∃ δ > 0, ∀ a ∈ s, dist a b < δ → dist (f a) (f b) < ε
source
theorem Metric.continuous_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} :
Continuous f ↔ ∀ (b : α), ∀ ε > 0, ∃ δ > 0, ∀ (a : α), dist a b < δ → dist (f a) (f b) < ε
source
theorem Metric.tendsto_nhds {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : Filter β} {u : β → α} {a : α} :
Filter.Tendsto u f (nhds a) ↔ ∀ ε > 0, ∀ᶠ (x : β) in f, dist (u x) a < ε
source
theorem Metric.continuousAt_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} :
ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhds b, dist (f x) (f b) < ε
source
theorem Metric.continuousWithinAt_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {b : β} {s : Set β} :
ContinuousWithinAt f s b ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, dist (f x) (f b) < ε
source
theorem Metric.continuousOn_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} {s : Set β} :
ContinuousOn f s ↔ ∀ b ∈ s, ∀ ε > 0, ∀ᶠ (x : β) in nhdsWithin b s, dist (f x) (f b) < ε
source
theorem Metric.continuous_iff' {α : Type u} {β : Type v} [PseudoMetricSpace α] [TopologicalSpace β] {f : β → α} :
Continuous f ↔ ∀ (a : β), ∀ ε > 0, ∀ᶠ (x : β) in nhds a, dist (f x) (f a) < ε
source
theorem Metric.tendsto_atTop {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] {u : β → α} {a : α} :
Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ (N : β), ∀ n ≥ N, dist (u n) a < ε
source
theorem Metric.tendsto_atTop' {α : Type u} {β : Type v} [PseudoMetricSpace α] [Nonempty β] [SemilatticeSup β] [NoMaxOrder β] {u : β → α} {a : α} :
Filter.Tendsto u Filter.atTop (nhds a) ↔ ∀ ε > 0, ∃ (N : β), ∀ n > N, dist (u n) a < ε

A variant of `tendsto_atTop` that uses `∃ N, ∀ n > N, ...` rather than `∃ N, ∀ n ≥ N, ...`

source
theorem Metric.isOpen_singleton_iff {α : Type u_3} [PseudoMetricSpace α] {x : α} :
IsOpen {x} ↔ ∃ ε > 0, ∀ (y : α), dist y x < ε → y = x
source
theorem Dense.exists_dist_lt {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : Dense s) (x : α) {ε : ℝ} (hε : 0 < ε) :
∃ y ∈ s, dist x y < ε
source
theorem DenseRange.exists_dist_lt {α : Type u} [PseudoMetricSpace α] {β : Type u_3} {f : β → α} (hf : DenseRange f) (x : α) {ε : ℝ} (hε : 0 < ε) :
∃ (y : β), dist x (f y) < ε
source
theorem Metric.uniformSpace_eq_bot {α : Type u} [PseudoMetricSpace α] :
PseudoMetricSpace.toUniformSpace = ⊥ ↔ ∃ (r : ℝ), 0 < r ∧ Pairwise fun (x1 x2 : α) => r ≤ dist x1 x2

(Pseudo) metric space has discrete `UniformSpace` structure iff the distances between distinct points are uniformly bounded away from zero.

source
theorem DiscreteTopology.of_forall_le_dist {α : Type u_3} [PseudoMetricSpace α] {r : ℝ} (hpos : 0 < r) (hr : Pairwise fun (x1 x2 : α) => r ≤ dist x1 x2) :
DiscreteTopology α

If the distances between distinct points in a (pseudo) metric space are uniformly bounded away from zero, then the space has discrete topology.

source
theorem Metric.uniformity_edist_aux {α : Type u_3} (d : α → α → NNReal) :
⨅ (ε : ℝ), ⨅ (_ : ε > 0), Filter.principal {p : α × α | ↑(d p.1 p.2) < ε} = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : α × α | ↑(d p.1 p.2) < ε}
source
theorem Metric.uniformity_edist {α : Type u} [PseudoMetricSpace α] :
uniformity α = ⨅ (ε : ENNReal), ⨅ (_ : ε > 0), Filter.principal {p : α × α | edist p.1 p.2 < ε}
source
@[instance 100]
instance PseudoMetricSpace.toPseudoEMetricSpace {α : Type u} [PseudoMetricSpace α] :
PseudoEMetricSpace α

A pseudometric space induces a pseudoemetric space

Equations

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

source
theorem Metric.eball_top_eq_univ {α : Type u} [PseudoMetricSpace α] (x : α) :
EMetric.ball x ⊤ = Set.univ

In a pseudometric space, an open ball of infinite radius is the whole space

source
@[simp]
theorem Metric.emetric_ball {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
EMetric.ball x (ENNReal.ofReal ε) = ball x ε

Balls defined using the distance or the edistance coincide

source
@[simp]
theorem Metric.emetric_ball_nnreal {α : Type u} [PseudoMetricSpace α] {x : α} {ε : NNReal} :
EMetric.ball x ↑ε = ball x ↑ε

Balls defined using the distance or the edistance coincide

source
theorem Metric.emetric_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} (h : 0 ≤ ε) :
EMetric.closedBall x (ENNReal.ofReal ε) = closedBall x ε

Closed balls defined using the distance or the edistance coincide

source
@[simp]
theorem Metric.emetric_closedBall_nnreal {α : Type u} [PseudoMetricSpace α] {x : α} {ε : NNReal} :
EMetric.closedBall x ↑ε = closedBall x ↑ε

Closed balls defined using the distance or the edistance coincide

source
@[simp]
theorem Metric.emetric_ball_top {α : Type u} [PseudoMetricSpace α] (x : α) :
EMetric.ball x ⊤ = Set.univ
source
@[reducible, inline]
abbrev PseudoMetricSpace.replaceUniformity {α : Type u_3} [U : UniformSpace α] (m : PseudoMetricSpace α) (H : uniformity α = uniformity α) :
PseudoMetricSpace α

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

Equations

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

Instances For

source
theorem PseudoMetricSpace.replaceUniformity_eq {α : Type u_3} [U : UniformSpace α] (m : PseudoMetricSpace α) (H : uniformity α = uniformity α) :
m.replaceUniformity H = m
source
@[reducible, inline]
abbrev PseudoMetricSpace.replaceTopology {γ : Type u_3} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ) (H : U = toUniformSpace.toTopologicalSpace) :
PseudoMetricSpace γ

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

Equations

- m.replaceTopology H = m.replaceUniformity ⋯

Instances For

source
theorem PseudoMetricSpace.replaceTopology_eq {γ : Type u_3} [U : TopologicalSpace γ] (m : PseudoMetricSpace γ) (H : U = toUniformSpace.toTopologicalSpace) :
m.replaceTopology H = m
source
@[reducible, inline]
abbrev PseudoEMetricSpace.toPseudoMetricSpaceOfDist {X : Type u_3} [e : PseudoEMetricSpace X] (dist : X → X → ℝ) (dist_nonneg : ∀ (x y : X), 0 ≤ dist x y) (h : ∀ (x y : X), edist x y = ENNReal.ofReal (dist x y)) :
PseudoMetricSpace X

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

Equations

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

Instances For

source
@[reducible, inline]
abbrev PseudoEMetricSpace.toPseudoMetricSpace {α : Type u} [PseudoEMetricSpace α] (h : ∀ (x y : α), edist x y ≠ ⊤) :
PseudoMetricSpace α

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.

Equations

- PseudoEMetricSpace.toPseudoMetricSpace h = PseudoEMetricSpace.toPseudoMetricSpaceOfDist (fun (x1 x2 : α) => (edist x1 x2).toReal) ⋯ ⋯

Instances For

source
@[reducible, inline]
abbrev PseudoMetricSpace.replaceBornology {α : Type u_3} [B : Bornology α] (m : PseudoMetricSpace α) (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) :
PseudoMetricSpace α

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

Equations

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

Instances For

source
theorem PseudoMetricSpace.replaceBornology_eq {α : Type u_3} [m : PseudoMetricSpace α] [B : Bornology α] (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s) :
m.replaceBornology H = m
source
instance Real.pseudoMetricSpace :
PseudoMetricSpace ℝ

Instantiate the reals as a pseudometric space.

Equations

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

source
theorem Real.dist_eq (x y : ℝ) :
dist x y = |x - y|
source
theorem Real.nndist_eq (x y : ℝ) :
nndist x y = nnabs (x - y)
source
theorem Real.nndist_eq' (x y : ℝ) :
nndist x y = nnabs (y - x)
source
theorem Real.dist_0_eq_abs (x : ℝ) :
dist x 0 = |x|
source
theorem Real.sub_le_dist (x y : ℝ) :
x - y ≤ dist x y
source
theorem Real.ball_eq_Ioo (x r : ℝ) :
Metric.ball x r = Set.Ioo (x - r) (x + r)
source
theorem Real.closedBall_eq_Icc {x r : ℝ} :
Metric.closedBall x r = Set.Icc (x - r) (x + r)
source
theorem Real.Ioo_eq_ball (x y : ℝ) :
Set.Ioo x y = Metric.ball ((x + y) / 2) ((y - x) / 2)
source
theorem Real.Icc_eq_closedBall (x y : ℝ) :
Set.Icc x y = Metric.closedBall ((x + y) / 2) ((y - x) / 2)
source
theorem Metric.uniformity_eq_comap_nhds_zero {α : Type u} [PseudoMetricSpace α] :
uniformity α = Filter.comap (fun (p : α × α) => dist p.1 p.2) (nhds 0)
source
theorem tendsto_uniformity_iff_dist_tendsto_zero {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f : ι → α × α} {p : Filter ι} :
Filter.Tendsto f p (uniformity α) ↔ Filter.Tendsto (fun (x : ι) => dist (f x).1 (f x).2) p (nhds 0)
source
theorem Filter.Tendsto.congr_dist {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α} (h₁ : Tendsto f₁ p (nhds a)) (h : Tendsto (fun (x : ι) => dist (f₁ x) (f₂ x)) p (nhds 0)) :
Tendsto f₂ p (nhds a)
source
theorem tendsto_of_tendsto_of_dist {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α} (h₁ : Filter.Tendsto f₁ p (nhds a)) (h : Filter.Tendsto (fun (x : ι) => dist (f₁ x) (f₂ x)) p (nhds 0)) :
Filter.Tendsto f₂ p (nhds a)

Alias of `Filter.Tendsto.congr_dist`.

source
theorem tendsto_iff_of_dist {α : Type u} {ι : Type u_2} [PseudoMetricSpace α] {f₁ f₂ : ι → α} {p : Filter ι} {a : α} (h : Filter.Tendsto (fun (x : ι) => dist (f₁ x) (f₂ x)) p (nhds 0)) :
Filter.Tendsto f₁ p (nhds a) ↔ Filter.Tendsto f₂ p (nhds a)
source
theorem PseudoMetricSpace.dist_eq_of_dist_zero {α : Type u} [PseudoMetricSpace α] (x : α) {y z : α} (h : dist y z = 0) :
dist x y = dist x z
source
theorem dist_dist_dist_le_left {α : Type u} [PseudoMetricSpace α] (x y z : α) :
dist (dist x z) (dist y z) ≤ dist x y
source
theorem dist_dist_dist_le_right {α : Type u} [PseudoMetricSpace α] (x y z : α) :
dist (dist x y) (dist x z) ≤ dist y z
source
theorem dist_dist_dist_le {α : Type u} [PseudoMetricSpace α] (x y x' y' : α) :
dist (dist x y) (dist x' y') ≤ dist x x' + dist y y'
source
theorem nhds_comap_dist {α : Type u} [PseudoMetricSpace α] (a : α) :
Filter.comap (fun (x : α) => dist x a) (nhds 0) = nhds a
source
theorem tendsto_iff_dist_tendsto_zero {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} {x : Filter β} {a : α} :
Filter.Tendsto f x (nhds a) ↔ Filter.Tendsto (fun (b : β) => dist (f b) a) x (nhds 0)
source
theorem Metric.ball_subset_interior_closedBall {α : Type u} [PseudoMetricSpace α] {x : α} {ε : ℝ} :
ball x ε ⊆ interior (closedBall x ε)
source
theorem Metric.mem_closure_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} {a : α} :
a ∈ closure s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

ε-characterization of the closure in pseudometric spaces

source
theorem Metric.mem_closure_range_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {e : β → α} {a : α} :
a ∈ closure (Set.range e) ↔ ∀ ε > 0, ∃ (k : β), dist a (e k) < ε
source
theorem Metric.mem_closure_range_iff_nat {α : Type u} {β : Type v} [PseudoMetricSpace α] {e : β → α} {a : α} :
a ∈ closure (Set.range e) ↔ ∀ (n : ℕ), ∃ (k : β), dist a (e k) < 1 / (↑n + 1)
source
theorem Metric.mem_of_closed' {α : Type u} [PseudoMetricSpace α] {s : Set α} (hs : IsClosed s) {a : α} :
a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε
source
theorem Metric.dense_iff {α : Type u} [PseudoMetricSpace α] {s : Set α} :
Dense s ↔ ∀ (x : α), ∀ r > 0, (ball x r ∩ s).Nonempty
source
theorem Metric.dense_iff_iUnion_ball {α : Type u} [PseudoMetricSpace α] (s : Set α) :
Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = Set.univ
source
theorem Metric.denseRange_iff {α : Type u} {β : Type v} [PseudoMetricSpace α] {f : β → α} :
DenseRange f ↔ ∀ (x : α), ∀ r > 0, ∃ (y : β), dist x (f y) < r
source
instance instPseudoMetricSpaceAdditive {α : Type u} [PseudoMetricSpace α] :
PseudoMetricSpace (Additive α)
Equations

- instPseudoMetricSpaceAdditive = inst✝

source
instance instPseudoMetricSpaceMultiplicative {α : Type u} [PseudoMetricSpace α] :
PseudoMetricSpace (Multiplicative α)
Equations

- instPseudoMetricSpaceMultiplicative = inst✝

source
@[simp]
theorem nndist_ofMul {X : Type u_1} [PseudoMetricSpace X] (a b : X) :
nndist (Additive.ofMul a) (Additive.ofMul b) = nndist a b
source
@[simp]
theorem nndist_ofAdd {X : Type u_1} [PseudoMetricSpace X] (a b : X) :
nndist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = nndist a b
source
@[simp]
theorem nndist_toMul {X : Type u_1} [PseudoMetricSpace X] (a b : Additive X) :
nndist (Additive.toMul a) (Additive.toMul b) = nndist a b
source
@[simp]
theorem nndist_toAdd {X : Type u_1} [PseudoMetricSpace X] (a b : Multiplicative X) :
nndist (Multiplicative.toAdd a) (Multiplicative.toAdd b) = nndist a b
source
instance instPseudoMetricSpaceOrderDual {α : Type u} [PseudoMetricSpace α] :
PseudoMetricSpace α ᵒᵈ
Equations

- instPseudoMetricSpaceOrderDual = inst✝

source
@[simp]
theorem nndist_toDual {X : Type u_1} [PseudoMetricSpace X] (a b : X) :
nndist (OrderDual.toDual a) (OrderDual.toDual b) = nndist a b
source
@[simp]
theorem nndist_ofDual {X : Type u_1} [PseudoMetricSpace X] (a b : X ᵒᵈ) :
nndist (OrderDual.ofDual a) (OrderDual.ofDual b) = nndist a b