Metric spaces #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines metric spaces. Many definitions and theorems expected on 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 #
has_dist α: Endows a spaceαwith a functiondist a b.pseudo_metric_space α: 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 pointsywithdist y x < ε.metric.bounded s: Whether a subset of apseudo_metric_spaceis bounded.metric_space α: Apseudo_metric_spacewith the guaranteedist x y = 0 → x = y.
Additional useful definitions:
nndist a b:distas a function to the non-negative reals.metric.closed_ball x ε: The set of all pointsywithdist y x ≤ ε.metric.sphere x ε: The set of all pointsywithdist y x = ε.proper_space α: Apseudo_metric_spacewhere all closed balls are compact.metric.diam s: Thesuprof the distances of members ofs. Defined in terms ofemetric.diam, for better handling of the case when it should be infinite.
TODO (anyone): Add "Main results" section.
Implementation notes #
Since a lot of elementary properties don't require eq_of_dist_eq_zero we start setting up the
theory of pseudo_metric_space, where we don't require dist x y = 0 → x = y and we specialize
to metric_space at the end.
Tags #
metric, pseudo_metric, dist
def
uniform_space_of_dist
{α : 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) :
Construct a uniform structure from a distance function and metric space axioms
Equations
- uniform_space_of_dist dist dist_self dist_comm dist_triangle = uniform_space.of_fun dist dist_self dist_comm dist_triangle uniform_space_of_dist._proof_1
@[ext, class]
The distance function (given an ambient metric space on α), which returns
a nonnegative real number dist x y given x y : α.
Instances of this typeclass
Instances of other typeclasses for has_dist
- has_dist.has_sizeof_inst
@[class]
- to_has_dist : has_dist α
- dist_self : ∀ (x : α), has_dist.dist x x = 0
- dist_comm : ∀ (x y : α), has_dist.dist x y = has_dist.dist y x
- dist_triangle : ∀ (x y z : α), has_dist.dist x z ≤ has_dist.dist x y + has_dist.dist y z
- edist : α → α → ennreal
- edist_dist : (∀ (x y : α), pseudo_metric_space.edist x y = ennreal.of_real (has_dist.dist x y)) . "edist_dist_tac"
- to_uniform_space : uniform_space α
- uniformity_dist : (uniformity α = ⨅ (ε : ℝ) (H : ε > 0), filter.principal {p : α × α | has_dist.dist p.fst p.snd < ε}) . "control_laws_tac"
- to_bornology : bornology α
- cobounded_sets : (bornology.cobounded α).sets = {s : set α | ∃ (C : ℝ), ∀ ⦃x : α⦄, x ∈ sᶜ → ∀ ⦃y : α⦄, y ∈ sᶜ → has_dist.dist x y ≤ C} . "control_laws_tac"
Pseudo metric and Metric spaces
A pseudo metric space is endowed with a distance for which the requirement d(x,y)=0 → x = y might
not hold. A metric space is a pseudo metric space such that d(x,y)=0 → x = y.
Each pseudo metric space induces a canonical uniform_space and hence a canonical
topological_space This is enforced in the type class definition, by extending the uniform_space
structure. When instantiating a pseudo_metric_space structure, the uniformity fields are not
necessary, they will be filled in by default. In the same way, each (pseudo) metric space induces a
(pseudo) emetric space structure. It is included in the structure, but filled in by default.
Instances of this typeclass
- metric_space.to_pseudo_metric_space
- seminormed_add_group.to_pseudo_metric_space
- seminormed_group.to_pseudo_metric_space
- seminormed_add_comm_group.to_pseudo_metric_space
- seminormed_comm_group.to_pseudo_metric_space
- non_unital_semi_normed_ring.to_pseudo_metric_space
- semi_normed_ring.to_pseudo_metric_space
- real.pseudo_metric_space
- subtype.pseudo_metric_space
- mul_opposite.pseudo_metric_space
- add_opposite.pseudo_metric_space
- nnreal.pseudo_metric_space
- ulift.pseudo_metric_space
- prod.pseudo_metric_space_max
- pseudo_metric_space_pi
- additive.pseudo_metric_space
- multiplicative.pseudo_metric_space
- order_dual.pseudo_metric_space
- continuous_linear_map.to_pseudo_metric_space
- pi_Lp.pseudo_metric_space
Instances of other typeclasses for pseudo_metric_space
- pseudo_metric_space.has_sizeof_inst
@[ext]
theorem
pseudo_metric_space.ext
{α : Type u_1}
{m m' : pseudo_metric_space α}
(h : pseudo_metric_space.to_has_dist = pseudo_metric_space.to_has_dist) :
m = m'
Two pseudo metric space structures with the same distance function coincide.
@[protected, instance]
Equations
def
pseudo_metric_space.of_dist_topology
{α : Type u}
[topological_space α]
(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 α), is_open s ↔ ∀ (x : α), x ∈ s → (∃ (ε : ℝ) (H : ε > 0), ∀ (y : α), dist x y < ε → y ∈ s)) :
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
- pseudo_metric_space.of_dist_topology dist dist_self dist_comm dist_triangle H = {to_has_dist := {dist := dist}, dist_self := dist_self, dist_comm := dist_comm, dist_triangle := dist_triangle, edist := λ (x y : α), ↑⟨dist x y, _⟩, edist_dist := _, to_uniform_space := {to_topological_space := _inst_2, to_core := uniform_space.to_core (uniform_space_of_dist dist dist_self dist_comm dist_triangle), is_open_uniformity := _}, uniformity_dist := _, to_bornology := bornology.of_dist dist dist_self dist_comm dist_triangle, cobounded_sets := _}
@[simp]
theorem
dist_comm
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
has_dist.dist x y = has_dist.dist y x
theorem
edist_dist
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
has_edist.edist x y = ennreal.of_real (has_dist.dist x y)
theorem
dist_triangle
{α : Type u}
[pseudo_metric_space α]
(x y z : α) :
has_dist.dist x z ≤ has_dist.dist x y + has_dist.dist y z
theorem
dist_triangle_left
{α : Type u}
[pseudo_metric_space α]
(x y z : α) :
has_dist.dist x y ≤ has_dist.dist z x + has_dist.dist z y
theorem
dist_triangle_right
{α : Type u}
[pseudo_metric_space α]
(x y z : α) :
has_dist.dist x y ≤ has_dist.dist x z + has_dist.dist y z
theorem
dist_triangle4
{α : Type u}
[pseudo_metric_space α]
(x y z w : α) :
has_dist.dist x w ≤ has_dist.dist x y + has_dist.dist y z + has_dist.dist z w
theorem
dist_triangle4_left
{α : Type u}
[pseudo_metric_space α]
(x₁ y₁ x₂ y₂ : α) :
has_dist.dist x₂ y₂ ≤ has_dist.dist x₁ y₁ + (has_dist.dist x₁ x₂ + has_dist.dist y₁ y₂)
theorem
dist_triangle4_right
{α : Type u}
[pseudo_metric_space α]
(x₁ y₁ x₂ y₂ : α) :
has_dist.dist x₁ y₁ ≤ has_dist.dist x₁ x₂ + has_dist.dist y₁ y₂ + has_dist.dist x₂ y₂
theorem
dist_le_Ico_sum_dist
{α : Type u}
[pseudo_metric_space α]
(f : ℕ → α)
{m n : ℕ}
(h : m ≤ n) :
has_dist.dist (f m) (f n) ≤ (finset.Ico m n).sum (λ (i : ℕ), has_dist.dist (f i) (f (i + 1)))
The triangle (polygon) inequality for sequences of points; finset.Ico version.
theorem
dist_le_range_sum_dist
{α : Type u}
[pseudo_metric_space α]
(f : ℕ → α)
(n : ℕ) :
has_dist.dist (f 0) (f n) ≤ (finset.range n).sum (λ (i : ℕ), has_dist.dist (f i) (f (i + 1)))
The triangle (polygon) inequality for sequences of points; finset.range version.
theorem
dist_le_Ico_sum_of_dist_le
{α : Type u}
[pseudo_metric_space α]
{f : ℕ → α}
{m n : ℕ}
(hmn : m ≤ n)
{d : ℕ → ℝ}
(hd : ∀ {k : ℕ}, m ≤ k → k < n → has_dist.dist (f k) (f (k + 1)) ≤ d k) :
has_dist.dist (f m) (f n) ≤ (finset.Ico m n).sum (λ (i : ℕ), d i)
A version of dist_le_Ico_sum_dist with each intermediate distance replaced
with an upper estimate.
theorem
dist_le_range_sum_of_dist_le
{α : Type u}
[pseudo_metric_space α]
{f : ℕ → α}
(n : ℕ)
{d : ℕ → ℝ}
(hd : ∀ {k : ℕ}, k < n → has_dist.dist (f k) (f (k + 1)) ≤ d k) :
has_dist.dist (f 0) (f n) ≤ (finset.range n).sum (λ (i : ℕ), d i)
A version of dist_le_range_sum_dist with each intermediate distance replaced
with an upper estimate.
theorem
abs_dist_sub_le
{α : Type u}
[pseudo_metric_space α]
(x y z : α) :
|has_dist.dist x z - has_dist.dist y z| ≤ has_dist.dist x y
@[simp]
theorem
abs_dist
{α : Type u}
[pseudo_metric_space α]
{a b : α} :
|has_dist.dist a b| = has_dist.dist a b
@[class]
A version of has_dist that takes value in ℝ≥0.
Instances of this typeclass
Instances of other typeclasses for has_nndist
- has_nndist.has_sizeof_inst
@[protected, instance]
Distance as a nonnegative real number.
Equations
- pseudo_metric_space.to_has_nndist = {nndist := λ (a b : α), ⟨has_dist.dist a b, _⟩}
theorem
nndist_edist
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
has_nndist.nndist x y = (has_edist.edist x y).to_nnreal
Express nndist in terms of edist
theorem
edist_nndist
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
has_edist.edist x y = ↑(has_nndist.nndist x y)
Express edist in terms of nndist
@[simp, norm_cast]
theorem
coe_nnreal_ennreal_nndist
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
↑(has_nndist.nndist x y) = has_edist.edist x y
@[simp, norm_cast]
theorem
edist_lt_coe
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{c : nnreal} :
has_edist.edist x y < ↑c ↔ has_nndist.nndist x y < c
@[simp, norm_cast]
theorem
edist_le_coe
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{c : nnreal} :
has_edist.edist x y ≤ ↑c ↔ has_nndist.nndist x y ≤ c
In a pseudometric space, the extended distance is always finite
In a pseudometric space, the extended distance is always finite
@[simp]
nndist x x vanishes
theorem
dist_nndist
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
has_dist.dist x y = ↑(has_nndist.nndist x y)
Express dist in terms of nndist
@[simp, norm_cast]
theorem
coe_nndist
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
↑(has_nndist.nndist x y) = has_dist.dist x y
@[simp, norm_cast]
theorem
dist_lt_coe
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{c : nnreal} :
has_dist.dist x y < ↑c ↔ has_nndist.nndist x y < c
@[simp, norm_cast]
theorem
dist_le_coe
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{c : nnreal} :
has_dist.dist x y ≤ ↑c ↔ has_nndist.nndist x y ≤ c
@[simp]
theorem
edist_lt_of_real
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{r : ℝ} :
has_edist.edist x y < ennreal.of_real r ↔ has_dist.dist x y < r
@[simp]
theorem
edist_le_of_real
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{r : ℝ}
(hr : 0 ≤ r) :
has_edist.edist x y ≤ ennreal.of_real r ↔ has_dist.dist x y ≤ r
theorem
nndist_dist
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
has_nndist.nndist x y = (has_dist.dist x y).to_nnreal
Express nndist in terms of dist
theorem
nndist_comm
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
has_nndist.nndist x y = has_nndist.nndist y x
theorem
nndist_triangle
{α : Type u}
[pseudo_metric_space α]
(x y z : α) :
has_nndist.nndist x z ≤ has_nndist.nndist x y + has_nndist.nndist y z
Triangle inequality for the nonnegative distance
theorem
nndist_triangle_left
{α : Type u}
[pseudo_metric_space α]
(x y z : α) :
has_nndist.nndist x y ≤ has_nndist.nndist z x + has_nndist.nndist z y
theorem
nndist_triangle_right
{α : Type u}
[pseudo_metric_space α]
(x y z : α) :
has_nndist.nndist x y ≤ has_nndist.nndist x z + has_nndist.nndist y z
theorem
dist_edist
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
has_dist.dist x y = (has_edist.edist x y).to_real
Express dist in terms of edist
ball x ε is the set of all points y with dist y x < ε
Equations
- metric.ball x ε = {y : α | has_dist.dist y x < ε}
@[simp]
theorem
metric.mem_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ} :
y ∈ metric.ball x ε ↔ has_dist.dist y x < ε
theorem
metric.mem_ball'
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ} :
y ∈ metric.ball x ε ↔ has_dist.dist x y < ε
theorem
metric.pos_of_mem_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ}
(hy : y ∈ metric.ball x ε) :
0 < ε
theorem
metric.mem_ball_self
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ}
(h : 0 < ε) :
x ∈ metric.ball x ε
@[simp]
theorem
metric.nonempty_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
(metric.ball x ε).nonempty ↔ 0 < ε
@[simp]
theorem
metric.ball_eq_empty
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
metric.ball x ε = ∅ ↔ ε ≤ 0
@[simp]
theorem
metric.exists_lt_mem_ball_of_mem_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ}
(h : x ∈ metric.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.
theorem
metric.ball_eq_ball
{α : Type u}
[pseudo_metric_space α]
(ε : ℝ)
(x : α) :
uniform_space.ball x {p : α × α | has_dist.dist p.snd p.fst < ε} = metric.ball x ε
theorem
metric.ball_eq_ball'
{α : Type u}
[pseudo_metric_space α]
(ε : ℝ)
(x : α) :
uniform_space.ball x {p : α × α | has_dist.dist p.fst p.snd < ε} = metric.ball x ε
@[simp]
@[simp]
closed_ball x ε is the set of all points y with dist y x ≤ ε
Equations
- metric.closed_ball x ε = {y : α | has_dist.dist y x ≤ ε}
@[simp]
theorem
metric.mem_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ} :
y ∈ metric.closed_ball x ε ↔ has_dist.dist y x ≤ ε
theorem
metric.mem_closed_ball'
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ} :
y ∈ metric.closed_ball x ε ↔ has_dist.dist x y ≤ ε
sphere x ε is the set of all points y with dist y x = ε
Equations
- metric.sphere x ε = {y : α | has_dist.dist y x = ε}
Instances for ↥metric.sphere
@[simp]
theorem
metric.mem_sphere
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ} :
y ∈ metric.sphere x ε ↔ has_dist.dist y x = ε
theorem
metric.mem_sphere'
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ} :
y ∈ metric.sphere x ε ↔ has_dist.dist x y = ε
theorem
metric.ne_of_mem_sphere
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ}
(h : y ∈ metric.sphere x ε)
(hε : ε ≠ 0) :
y ≠ x
theorem
metric.nonneg_of_mem_sphere
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ}
(hy : y ∈ metric.sphere x ε) :
0 ≤ ε
@[simp]
theorem
metric.sphere_eq_empty_of_neg
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ}
(hε : ε < 0) :
metric.sphere x ε = ∅
theorem
metric.sphere_eq_empty_of_subsingleton
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ}
[subsingleton α]
(hε : ε ≠ 0) :
metric.sphere x ε = ∅
theorem
metric.sphere_is_empty_of_subsingleton
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ}
[subsingleton α]
(hε : ε ≠ 0) :
is_empty ↥(metric.sphere x ε)
theorem
metric.mem_closed_ball_self
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ}
(h : 0 ≤ ε) :
x ∈ metric.closed_ball x ε
@[simp]
theorem
metric.nonempty_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
(metric.closed_ball x ε).nonempty ↔ 0 ≤ ε
@[simp]
theorem
metric.closed_ball_eq_empty
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
metric.closed_ball x ε = ∅ ↔ ε < 0
theorem
metric.closed_ball_eq_sphere_of_nonpos
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ}
(hε : ε ≤ 0) :
metric.closed_ball x ε = metric.sphere x ε
Closed balls and spheres coincide when the radius is non-positive
theorem
metric.ball_subset_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
metric.ball x ε ⊆ metric.closed_ball x ε
theorem
metric.sphere_subset_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
metric.sphere x ε ⊆ metric.closed_ball x ε
theorem
metric.closed_ball_disjoint_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{δ ε : ℝ}
(h : δ + ε ≤ has_dist.dist x y) :
disjoint (metric.closed_ball x δ) (metric.ball y ε)
theorem
metric.ball_disjoint_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{δ ε : ℝ}
(h : δ + ε ≤ has_dist.dist x y) :
disjoint (metric.ball x δ) (metric.closed_ball y ε)
theorem
metric.ball_disjoint_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{δ ε : ℝ}
(h : δ + ε ≤ has_dist.dist x y) :
disjoint (metric.ball x δ) (metric.ball y ε)
theorem
metric.closed_ball_disjoint_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{δ ε : ℝ}
(h : δ + ε < has_dist.dist x y) :
disjoint (metric.closed_ball x δ) (metric.closed_ball y ε)
theorem
metric.sphere_disjoint_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
disjoint (metric.sphere x ε) (metric.ball x ε)
@[simp]
theorem
metric.ball_union_sphere
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
metric.ball x ε ∪ metric.sphere x ε = metric.closed_ball x ε
@[simp]
theorem
metric.sphere_union_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
metric.sphere x ε ∪ metric.ball x ε = metric.closed_ball x ε
@[simp]
theorem
metric.closed_ball_diff_sphere
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
metric.closed_ball x ε \ metric.sphere x ε = metric.ball x ε
@[simp]
theorem
metric.closed_ball_diff_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
metric.closed_ball x ε \ metric.ball x ε = metric.sphere x ε
theorem
metric.mem_ball_comm
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ} :
x ∈ metric.ball y ε ↔ y ∈ metric.ball x ε
theorem
metric.mem_closed_ball_comm
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ} :
x ∈ metric.closed_ball y ε ↔ y ∈ metric.closed_ball x ε
theorem
metric.mem_sphere_comm
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ} :
x ∈ metric.sphere y ε ↔ y ∈ metric.sphere x ε
theorem
metric.ball_subset_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε₁ ε₂ : ℝ}
(h : ε₁ ≤ ε₂) :
metric.ball x ε₁ ⊆ metric.ball x ε₂
theorem
metric.closed_ball_eq_bInter_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
metric.closed_ball x ε = ⋂ (δ : ℝ) (H : δ > ε), metric.ball x δ
theorem
metric.ball_subset_ball'
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε₁ ε₂ : ℝ}
(h : ε₁ + has_dist.dist x y ≤ ε₂) :
metric.ball x ε₁ ⊆ metric.ball y ε₂
theorem
metric.closed_ball_subset_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε₁ ε₂ : ℝ}
(h : ε₁ ≤ ε₂) :
metric.closed_ball x ε₁ ⊆ metric.closed_ball x ε₂
theorem
metric.closed_ball_subset_closed_ball'
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε₁ ε₂ : ℝ}
(h : ε₁ + has_dist.dist x y ≤ ε₂) :
metric.closed_ball x ε₁ ⊆ metric.closed_ball y ε₂
theorem
metric.closed_ball_subset_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε₁ ε₂ : ℝ}
(h : ε₁ < ε₂) :
metric.closed_ball x ε₁ ⊆ metric.ball x ε₂
theorem
metric.closed_ball_subset_ball'
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε₁ ε₂ : ℝ}
(h : ε₁ + has_dist.dist x y < ε₂) :
metric.closed_ball x ε₁ ⊆ metric.ball y ε₂
theorem
metric.dist_le_add_of_nonempty_closed_ball_inter_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε₁ ε₂ : ℝ}
(h : (metric.closed_ball x ε₁ ∩ metric.closed_ball y ε₂).nonempty) :
has_dist.dist x y ≤ ε₁ + ε₂
theorem
metric.dist_lt_add_of_nonempty_closed_ball_inter_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε₁ ε₂ : ℝ}
(h : (metric.closed_ball x ε₁ ∩ metric.ball y ε₂).nonempty) :
has_dist.dist x y < ε₁ + ε₂
theorem
metric.dist_lt_add_of_nonempty_ball_inter_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε₁ ε₂ : ℝ}
(h : (metric.ball x ε₁ ∩ metric.closed_ball y ε₂).nonempty) :
has_dist.dist x y < ε₁ + ε₂
theorem
metric.dist_lt_add_of_nonempty_ball_inter_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε₁ ε₂ : ℝ}
(h : (metric.ball x ε₁ ∩ metric.ball y ε₂).nonempty) :
has_dist.dist x y < ε₁ + ε₂
@[simp]
theorem
metric.Union_inter_closed_ball_nat
{α : Type u}
[pseudo_metric_space α]
(s : set α)
(x : α) :
theorem
metric.ball_subset
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε₁ ε₂ : ℝ}
(h : has_dist.dist x y ≤ ε₂ - ε₁) :
metric.ball x ε₁ ⊆ metric.ball y ε₂
theorem
metric.ball_half_subset
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ}
(y : α)
(h : y ∈ metric.ball x (ε / 2)) :
metric.ball y (ε / 2) ⊆ metric.ball x ε
theorem
metric.exists_ball_subset_ball
{α : Type u}
[pseudo_metric_space α]
{x y : α}
{ε : ℝ}
(h : y ∈ metric.ball x ε) :
∃ (ε' : ℝ) (H : ε' > 0), metric.ball y ε' ⊆ metric.ball x ε
theorem
metric.forall_of_forall_mem_closed_ball
{α : Type u}
[pseudo_metric_space α]
(p : α → Prop)
(x : α)
(H : ∃ᶠ (R : ℝ) in filter.at_top, ∀ (y : α), y ∈ metric.closed_ball 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.
theorem
metric.forall_of_forall_mem_ball
{α : Type u}
[pseudo_metric_space α]
(p : α → Prop)
(x : α)
(H : ∃ᶠ (R : ℝ) in filter.at_top, ∀ (y : α), y ∈ metric.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.
theorem
metric.is_bounded_iff_eventually
{α : Type u}
[pseudo_metric_space α]
{s : set α} :
bornology.is_bounded s ↔ ∀ᶠ (C : ℝ) in filter.at_top, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → has_dist.dist x y ≤ C
theorem
metric.uniformity_basis_dist
{α : Type u}
[pseudo_metric_space α] :
(uniformity α).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {p : α × α | has_dist.dist p.fst p.snd < ε})
@[protected]
theorem
metric.mk_uniformity_basis
{α : Type u}
[pseudo_metric_space α]
{β : Type u_1}
{p : β → Prop}
{f : β → ℝ}
(hf₀ : ∀ (i : β), p i → 0 < f i)
(hf : ∀ ⦃ε : ℝ⦄, 0 < ε → (∃ (i : β) (hi : p i), f i ≤ ε)) :
(uniformity α).has_basis p (λ (i : β), {p : α × α | has_dist.dist p.fst p.snd < 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.
theorem
metric.uniformity_basis_dist_pow
{α : Type u}
[pseudo_metric_space α]
{r : ℝ}
(h0 : 0 < r)
(h1 : r < 1) :
@[protected]
theorem
metric.mk_uniformity_basis_le
{α : Type u}
[pseudo_metric_space α]
{β : Type u_1}
{p : β → Prop}
{f : β → ℝ}
(hf₀ : ∀ (x : β), p x → 0 < f x)
(hf : ∀ (ε : ℝ), 0 < ε → (∃ (x : β) (hx : p x), f x ≤ ε)) :
(uniformity α).has_basis p (λ (x : β), {p : α × α | has_dist.dist p.fst p.snd ≤ 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.
theorem
metric.uniformity_basis_dist_le
{α : Type u}
[pseudo_metric_space α] :
(uniformity α).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), {p : α × α | has_dist.dist p.fst p.snd ≤ ε})
Contant size closed neighborhoods of the diagonal form a basis of the uniformity filter.
theorem
metric.uniformity_basis_dist_le_pow
{α : Type u}
[pseudo_metric_space α]
{r : ℝ}
(h0 : 0 < r)
(h1 : r < 1) :
theorem
metric.dist_mem_uniformity
{α : Type u}
[pseudo_metric_space α]
{ε : ℝ}
(ε0 : 0 < ε) :
{p : α × α | has_dist.dist p.fst p.snd < ε} ∈ uniformity α
A constant size neighborhood of the diagonal is an entourage.
theorem
metric.uniform_continuous_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β} :
theorem
metric.uniform_continuous_on_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
{s : set α} :
theorem
metric.uniform_continuous_on_iff_le
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
{s : set α} :
theorem
metric.uniform_embedding_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β} :
uniform_embedding f ↔ function.injective f ∧ uniform_continuous f ∧ ∀ (δ : ℝ), δ > 0 → (∃ (ε : ℝ) (H : ε > 0), ∀ {a b : α}, has_dist.dist (f a) (f b) < ε → has_dist.dist a b < δ)
theorem
metric.controlled_of_uniform_embedding
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β} :
If a map between pseudometric spaces is a uniform embedding then the distance between f x
and f y is controlled in terms of the distance between x and y.
theorem
metric.totally_bounded_of_finite_discretization
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(H : ∀ (ε : ℝ), ε > 0 → (∃ (β : Type u) (_x : fintype β) (F : ↥s → β), ∀ (x y : ↥s), F x = F y → has_dist.dist ↑x ↑y < ε)) :
A pseudometric space is totally bounded if one can reconstruct up to any ε>0 any element of the space from finitely many data.
theorem
metric.finite_approx_of_totally_bounded
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(hs : totally_bounded s)
(ε : ℝ)
(H : ε > 0) :
theorem
metric.tendsto_uniformly_on_filter_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{ι : Type u_1}
{F : ι → β → α}
{f : β → α}
{p : filter ι}
{p' : filter β} :
Expressing uniform convergence using dist
theorem
metric.tendsto_locally_uniformly_on_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{ι : Type u_1}
[topological_space β]
{F : ι → β → α}
{f : β → α}
{p : filter ι}
{s : set β} :
Expressing locally uniform convergence on a set using dist.
theorem
metric.tendsto_uniformly_on_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{ι : Type u_1}
{F : ι → β → α}
{f : β → α}
{p : filter ι}
{s : set β} :
Expressing uniform convergence on a set using dist.
theorem
metric.tendsto_locally_uniformly_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{ι : Type u_1}
[topological_space β]
{F : ι → β → α}
{f : β → α}
{p : filter ι} :
Expressing locally uniform convergence using dist.
theorem
metric.tendsto_uniformly_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{ι : Type u_1}
{F : ι → β → α}
{f : β → α}
{p : filter ι} :
Expressing uniform convergence using dist.
theorem
metric.nhds_basis_ball
{α : Type u}
[pseudo_metric_space α]
{x : α} :
(nhds x).has_basis (λ (ε : ℝ), 0 < ε) (metric.ball x)
theorem
metric.eventually_prod_nhds_iff
{α : Type u}
{ι : Type u_2}
[pseudo_metric_space α]
{f : filter ι}
{x₀ : α}
{p : ι × α → Prop} :
A version of filter.eventually_prod_iff where the second filter consists of neighborhoods
in a pseudo-metric space.
theorem
metric.eventually_nhds_prod_iff
{ι : Type u_1}
{α : Type u_2}
[pseudo_metric_space α]
{f : filter ι}
{x₀ : α}
{p : α × ι → Prop} :
A version of filter.eventually_prod_iff where the first filter consists of neighborhoods
in a pseudo-metric space.
theorem
metric.nhds_basis_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α} :
(nhds x).has_basis (λ (ε : ℝ), 0 < ε) (metric.closed_ball x)
theorem
metric.nhds_basis_ball_pow
{α : Type u}
[pseudo_metric_space α]
{x : α}
{r : ℝ}
(h0 : 0 < r)
(h1 : r < 1) :
theorem
metric.nhds_basis_closed_ball_pow
{α : Type u}
[pseudo_metric_space α]
{x : α}
{r : ℝ}
(h0 : 0 < r)
(h1 : r < 1) :
theorem
metric.is_open_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
is_open (metric.ball x ε)
theorem
metric.ball_mem_nhds
{α : Type u}
[pseudo_metric_space α]
(x : α)
{ε : ℝ}
(ε0 : 0 < ε) :
metric.ball x ε ∈ nhds x
theorem
metric.closed_ball_mem_nhds
{α : Type u}
[pseudo_metric_space α]
(x : α)
{ε : ℝ}
(ε0 : 0 < ε) :
metric.closed_ball x ε ∈ nhds x
theorem
metric.closed_ball_mem_nhds_of_mem
{α : Type u}
[pseudo_metric_space α]
{x c : α}
{ε : ℝ}
(h : x ∈ metric.ball c ε) :
metric.closed_ball c ε ∈ nhds x
theorem
metric.nhds_within_basis_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{s : set α} :
(nhds_within x s).has_basis (λ (ε : ℝ), 0 < ε) (λ (ε : ℝ), metric.ball x ε ∩ s)
theorem
metric.mem_nhds_within_iff
{α : Type u}
[pseudo_metric_space α]
{x : α}
{s t : set α} :
s ∈ nhds_within x t ↔ ∃ (ε : ℝ) (H : ε > 0), metric.ball x ε ∩ t ⊆ s
theorem
metric.tendsto_nhds_within_nhds_within
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{s : set α}
[pseudo_metric_space β]
{t : set β}
{f : α → β}
{a : α}
{b : β} :
filter.tendsto f (nhds_within a s) (nhds_within b t) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, x ∈ s → has_dist.dist x a < δ → f x ∈ t ∧ has_dist.dist (f x) b < ε)
theorem
metric.tendsto_nhds_within_nhds
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{s : set α}
[pseudo_metric_space β]
{f : α → β}
{a : α}
{b : β} :
filter.tendsto f (nhds_within a s) (nhds b) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (δ : ℝ) (H : δ > 0), ∀ {x : α}, x ∈ s → has_dist.dist x a < δ → has_dist.dist (f x) b < ε)
theorem
metric.tendsto_nhds_nhds
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
{a : α}
{b : β} :
theorem
metric.continuous_at_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
{a : α} :
theorem
metric.continuous_within_at_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
{a : α}
{s : set α} :
theorem
metric.continuous_on_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
{s : set α} :
theorem
metric.continuous_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β} :
theorem
metric.tendsto_nhds
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f : filter β}
{u : β → α}
{a : α} :
theorem
metric.continuous_at_iff'
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{f : β → α}
{b : β} :
theorem
metric.continuous_within_at_iff'
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{f : β → α}
{b : β}
{s : set β} :
continuous_within_at f s b ↔ ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in nhds_within b s, has_dist.dist (f x) (f b) < ε)
theorem
metric.continuous_on_iff'
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{f : β → α}
{s : set β} :
continuous_on f s ↔ ∀ (b : β), b ∈ s → ∀ (ε : ℝ), ε > 0 → (∀ᶠ (x : β) in nhds_within b s, has_dist.dist (f x) (f b) < ε)
theorem
metric.continuous_iff'
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{f : β → α} :
theorem
metric.tendsto_at_top
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[nonempty β]
[semilattice_sup β]
{u : β → α}
{a : α} :
filter.tendsto u filter.at_top (nhds a) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : β), ∀ (n : β), n ≥ N → has_dist.dist (u n) a < ε)
theorem
metric.tendsto_at_top'
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[nonempty β]
[semilattice_sup β]
[no_max_order β]
{u : β → α}
{a : α} :
filter.tendsto u filter.at_top (nhds a) ↔ ∀ (ε : ℝ), ε > 0 → (∃ (N : β), ∀ (n : β), n > N → has_dist.dist (u n) a < ε)
A variant of tendsto_at_top that
uses ∃ N, ∀ n > N, ... rather than ∃ N, ∀ n ≥ N, ...
theorem
metric.exists_ball_inter_eq_singleton_of_mem_discrete
{α : Type u}
[pseudo_metric_space α]
{s : set α}
[discrete_topology ↥s]
{x : α}
(hx : x ∈ s) :
Given a point x in a discrete subset s of a pseudometric space, there is an open ball
centered at x and intersecting s only at x.
theorem
metric.exists_closed_ball_inter_eq_singleton_of_discrete
{α : Type u}
[pseudo_metric_space α]
{s : set α}
[discrete_topology ↥s]
{x : α}
(hx : x ∈ s) :
Given a point x in a discrete subset s of a pseudometric space, there is a closed ball
of positive radius centered at x and intersecting s only at x.
theorem
dense.exists_dist_lt
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(hs : dense s)
(x : α)
{ε : ℝ}
(hε : 0 < ε) :
∃ (y : α) (H : y ∈ s), has_dist.dist x y < ε
theorem
dense_range.exists_dist_lt
{α : Type u}
[pseudo_metric_space α]
{β : Type u_1}
{f : β → α}
(hf : dense_range f)
(x : α)
{ε : ℝ}
(hε : 0 < ε) :
∃ (y : β), has_dist.dist x (f y) < ε
@[protected]
theorem
pseudo_metric.uniformity_basis_edist
{α : Type u}
[pseudo_metric_space α] :
(uniformity α).has_basis (λ (ε : ennreal), 0 < ε) (λ (ε : ennreal), {p : α × α | has_edist.edist p.fst p.snd < ε})
Expressing the uniformity in terms of edist
theorem
metric.uniformity_edist
{α : Type u}
[pseudo_metric_space α] :
uniformity α = ⨅ (ε : ennreal) (H : ε > 0), filter.principal {p : α × α | has_edist.edist p.fst p.snd < ε}
@[protected, instance]
A pseudometric space induces a pseudoemetric space
Equations
- pseudo_metric_space.to_pseudo_emetric_space = {to_has_edist := {edist := has_edist.edist pseudo_metric_space.to_has_edist}, edist_self := _, edist_comm := _, edist_triangle := _, to_uniform_space := pseudo_metric_space.to_uniform_space _inst_1, uniformity_edist := _}
In a pseudometric space, an open ball of infinite radius is the whole space
@[simp]
theorem
metric.emetric_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
emetric.ball x (ennreal.of_real ε) = metric.ball x ε
Balls defined using the distance or the edistance coincide
@[simp]
theorem
metric.emetric_ball_nnreal
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : nnreal} :
emetric.ball x ↑ε = metric.ball x ↑ε
Balls defined using the distance or the edistance coincide
theorem
metric.emetric_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ}
(h : 0 ≤ ε) :
Closed balls defined using the distance or the edistance coincide
@[simp]
theorem
metric.emetric_closed_ball_nnreal
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : nnreal} :
emetric.closed_ball x ↑ε = metric.closed_ball x ↑ε
Closed balls defined using the distance or the edistance coincide
@[simp]
theorem
metric.inseparable_iff
{α : Type u}
[pseudo_metric_space α]
{x y : α} :
inseparable x y ↔ has_dist.dist x y = 0
def
pseudo_metric_space.replace_uniformity
{α : Type u_1}
[U : uniform_space α]
(m : pseudo_metric_space α)
(H : uniformity α = uniformity α) :
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].
Equations
- m.replace_uniformity H = {to_has_dist := {dist := has_dist.dist pseudo_metric_space.to_has_dist}, dist_self := _, dist_comm := _, dist_triangle := _, edist := has_edist.edist pseudo_metric_space.to_has_edist, edist_dist := _, to_uniform_space := U, uniformity_dist := _, to_bornology := bornology.of_dist has_dist.dist dist_self dist_comm dist_triangle, cobounded_sets := _}
theorem
pseudo_metric_space.replace_uniformity_eq
{α : Type u_1}
[U : uniform_space α]
(m : pseudo_metric_space α)
(H : uniformity α = uniformity α) :
m.replace_uniformity H = m
@[reducible]
def
pseudo_metric_space.replace_topology
{γ : Type u_1}
[U : topological_space γ]
(m : pseudo_metric_space γ)
(H : U = uniform_space.to_topological_space) :
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].
Equations
- m.replace_topology H = m.replace_uniformity _
theorem
pseudo_metric_space.replace_topology_eq
{γ : Type u_1}
[U : topological_space γ]
(m : pseudo_metric_space γ)
(H : U = uniform_space.to_topological_space) :
m.replace_topology H = m
def
pseudo_emetric_space.to_pseudo_metric_space_of_dist
{α : Type u}
[e : pseudo_emetric_space α]
(dist : α → α → ℝ)
(edist_ne_top : ∀ (x y : α), has_edist.edist x y ≠ ⊤)
(h : ∀ (x y : α), dist x y = (has_edist.edist x y).to_real) :
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.
Equations
- pseudo_emetric_space.to_pseudo_metric_space_of_dist dist edist_ne_top h = let m : pseudo_metric_space α := {to_has_dist := {dist := dist}, dist_self := _, dist_comm := _, dist_triangle := _, edist := has_edist.edist pseudo_emetric_space.to_has_edist, edist_dist := _, to_uniform_space := uniform_space_of_dist dist _ _ _, uniformity_dist := _, to_bornology := bornology.of_dist dist _ _ _, cobounded_sets := _} in m.replace_uniformity _
def
pseudo_emetric_space.to_pseudo_metric_space
{α : Type u}
[e : pseudo_emetric_space α]
(h : ∀ (x y : α), has_edist.edist x y ≠ ⊤) :
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
- pseudo_emetric_space.to_pseudo_metric_space h = pseudo_emetric_space.to_pseudo_metric_space_of_dist (λ (x y : α), (has_edist.edist x y).to_real) h pseudo_emetric_space.to_pseudo_metric_space._proof_1
def
pseudo_metric_space.replace_bornology
{α : Type u_1}
[B : bornology α]
(m : pseudo_metric_space α)
(H : ∀ (s : set α), bornology.is_bounded s ↔ bornology.is_bounded s) :
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].
Equations
- m.replace_bornology H = {to_has_dist := pseudo_metric_space.to_has_dist m, dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist m, edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space m, uniformity_dist := _, to_bornology := B, cobounded_sets := _}
theorem
pseudo_metric_space.replace_bornology_eq
{α : Type u_1}
[m : pseudo_metric_space α]
[B : bornology α]
(H : ∀ (s : set α), bornology.is_bounded s ↔ bornology.is_bounded s) :
m.replace_bornology H = m
theorem
metric.complete_of_convergent_controlled_sequences
{α : Type u}
[pseudo_metric_space α]
(B : ℕ → ℝ)
(hB : ∀ (n : ℕ), 0 < B n)
(H : ∀ (u : ℕ → α), (∀ (N n m : ℕ), N ≤ n → N ≤ m → has_dist.dist (u n) (u m) < B N) → (∃ (x : α), filter.tendsto u filter.at_top (nhds x))) :
A very useful criterion to show that a space is complete is to show that all sequences
which satisfy a bound of the form dist (u n) (u m) < B N for all n m ≥ N are
converging. This is often applied for B N = 2^{-N}, i.e., with a very fast convergence to
0, which makes it possible to use arguments of converging series, while this is impossible
to do in general for arbitrary Cauchy sequences.
theorem
metric.complete_of_cauchy_seq_tendsto
{α : Type u}
[pseudo_metric_space α] :
(∀ (u : ℕ → α), cauchy_seq u → (∃ (a : α), filter.tendsto u filter.at_top (nhds a))) → complete_space α
@[protected, instance]
Instantiate the reals as a pseudometric space.
Equations
- real.pseudo_metric_space = {to_has_dist := {dist := λ (x y : ℝ), |x - y|}, dist_self := real.pseudo_metric_space._proof_1, dist_comm := real.pseudo_metric_space._proof_2, dist_triangle := real.pseudo_metric_space._proof_3, edist := λ (x y : ℝ), ↑⟨(λ (x y : ℝ), |x - y|) x y, _⟩, edist_dist := real.pseudo_metric_space._proof_5, to_uniform_space := uniform_space_of_dist (λ (x y : ℝ), |x - y|) real.pseudo_metric_space._proof_6 real.pseudo_metric_space._proof_7 real.pseudo_metric_space._proof_8, uniformity_dist := real.pseudo_metric_space._proof_9, to_bornology := bornology.of_dist (λ (x y : ℝ), |x - y|) real.pseudo_metric_space._proof_10 real.pseudo_metric_space._proof_11 real.pseudo_metric_space._proof_12, cobounded_sets := real.pseudo_metric_space._proof_13}
theorem
real.dist_left_le_of_mem_uIcc
{x y z : ℝ}
(h : y ∈ set.uIcc x z) :
has_dist.dist x y ≤ has_dist.dist x z
theorem
real.dist_right_le_of_mem_uIcc
{x y z : ℝ}
(h : y ∈ set.uIcc x z) :
has_dist.dist y z ≤ has_dist.dist x z
theorem
real.dist_le_of_mem_uIcc
{x y x' y' : ℝ}
(hx : x ∈ set.uIcc x' y')
(hy : y ∈ set.uIcc x' y') :
has_dist.dist x y ≤ has_dist.dist x' y'
theorem
real.dist_le_of_mem_Icc
{x y x' y' : ℝ}
(hx : x ∈ set.Icc x' y')
(hy : y ∈ set.Icc x' y') :
has_dist.dist x y ≤ y' - x'
theorem
real.dist_le_of_mem_Icc_01
{x y : ℝ}
(hx : x ∈ set.Icc 0 1)
(hy : y ∈ set.Icc 0 1) :
has_dist.dist x y ≤ 1
theorem
totally_bounded_Icc
{α : Type u}
[pseudo_metric_space α]
[preorder α]
[compact_Icc_space α]
(a b : α) :
totally_bounded (set.Icc a b)
theorem
totally_bounded_Ico
{α : Type u}
[pseudo_metric_space α]
[preorder α]
[compact_Icc_space α]
(a b : α) :
totally_bounded (set.Ico a b)
theorem
totally_bounded_Ioc
{α : Type u}
[pseudo_metric_space α]
[preorder α]
[compact_Icc_space α]
(a b : α) :
totally_bounded (set.Ioc a b)
theorem
totally_bounded_Ioo
{α : Type u}
[pseudo_metric_space α]
[preorder α]
[compact_Icc_space α]
(a b : α) :
totally_bounded (set.Ioo a b)
theorem
squeeze_zero'
{α : Type u_1}
{f g : α → ℝ}
{t₀ : filter α}
(hf : ∀ᶠ (t : α) in t₀, 0 ≤ f t)
(hft : ∀ᶠ (t : α) in t₀, f t ≤ g t)
(g0 : filter.tendsto g t₀ (nhds 0)) :
filter.tendsto f t₀ (nhds 0)
Special case of the sandwich theorem; see tendsto_of_tendsto_of_tendsto_of_le_of_le' for the
general case.
theorem
squeeze_zero
{α : Type u_1}
{f g : α → ℝ}
{t₀ : filter α}
(hf : ∀ (t : α), 0 ≤ f t)
(hft : ∀ (t : α), f t ≤ g t)
(g0 : filter.tendsto g t₀ (nhds 0)) :
filter.tendsto f t₀ (nhds 0)
Special case of the sandwich theorem; see tendsto_of_tendsto_of_tendsto_of_le_of_le
and tendsto_of_tendsto_of_tendsto_of_le_of_le' for the general case.
theorem
metric.uniformity_eq_comap_nhds_zero
{α : Type u}
[pseudo_metric_space α] :
uniformity α = filter.comap (λ (p : α × α), has_dist.dist p.fst p.snd) (nhds 0)
theorem
cauchy_seq_iff_tendsto_dist_at_top_0
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[nonempty β]
[semilattice_sup β]
{u : β → α} :
cauchy_seq u ↔ filter.tendsto (λ (n : β × β), has_dist.dist (u n.fst) (u n.snd)) filter.at_top (nhds 0)
theorem
tendsto_uniformity_iff_dist_tendsto_zero
{α : Type u}
[pseudo_metric_space α]
{ι : Type u_1}
{f : ι → α × α}
{p : filter ι} :
filter.tendsto f p (uniformity α) ↔ filter.tendsto (λ (x : ι), has_dist.dist (f x).fst (f x).snd) p (nhds 0)
theorem
filter.tendsto.congr_dist
{α : Type u}
[pseudo_metric_space α]
{ι : Type u_1}
{f₁ f₂ : ι → α}
{p : filter ι}
{a : α}
(h₁ : filter.tendsto f₁ p (nhds a))
(h : filter.tendsto (λ (x : ι), has_dist.dist (f₁ x) (f₂ x)) p (nhds 0)) :
filter.tendsto f₂ p (nhds a)
theorem
tendsto_of_tendsto_of_dist
{α : Type u}
[pseudo_metric_space α]
{ι : Type u_1}
{f₁ f₂ : ι → α}
{p : filter ι}
{a : α}
(h₁ : filter.tendsto f₁ p (nhds a))
(h : filter.tendsto (λ (x : ι), has_dist.dist (f₁ x) (f₂ x)) p (nhds 0)) :
filter.tendsto f₂ p (nhds a)
Alias of filter.tendsto.congr_dist.
theorem
tendsto_iff_of_dist
{α : Type u}
[pseudo_metric_space α]
{ι : Type u_1}
{f₁ f₂ : ι → α}
{p : filter ι}
{a : α}
(h : filter.tendsto (λ (x : ι), has_dist.dist (f₁ x) (f₂ x)) p (nhds 0)) :
filter.tendsto f₁ p (nhds a) ↔ filter.tendsto f₂ p (nhds a)
theorem
eventually_closed_ball_subset
{α : Type u}
[pseudo_metric_space α]
{x : α}
{u : set α}
(hu : u ∈ nhds x) :
If u is a neighborhood of x, then for small enough r, the closed ball
closed_ball x r is contained in u.
@[nolint]
theorem
metric.cauchy_seq_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[nonempty β]
[semilattice_sup β]
{u : β → α} :
In a pseudometric space, Cauchy sequences are characterized by the fact that, eventually, the distance between its elements is arbitrarily small
theorem
metric.cauchy_seq_iff'
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[nonempty β]
[semilattice_sup β]
{u : β → α} :
A variation around the pseudometric characterization of Cauchy sequences
@[nolint]
theorem
metric.uniform_cauchy_seq_on_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[nonempty β]
[semilattice_sup β]
{γ : Type u_1}
{F : β → γ → α}
{s : set γ} :
In a pseudometric space, unifom Cauchy sequences are characterized by the fact that, eventually, the distance between all its elements is uniformly, arbitrarily small
theorem
cauchy_seq_of_le_tendsto_0'
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[nonempty β]
[semilattice_sup β]
{s : β → α}
(b : β → ℝ)
(h : ∀ (n m : β), n ≤ m → has_dist.dist (s n) (s m) ≤ b n)
(h₀ : filter.tendsto b filter.at_top (nhds 0)) :
If the distance between s n and s m, n ≤ m is bounded above by b n
and b converges to zero, then s is a Cauchy sequence.
theorem
cauchy_seq_of_le_tendsto_0
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[nonempty β]
[semilattice_sup β]
{s : β → α}
(b : β → ℝ)
(h : ∀ (n m N : β), N ≤ n → N ≤ m → has_dist.dist (s n) (s m) ≤ b N)
(h₀ : filter.tendsto b filter.at_top (nhds 0)) :
If the distance between s n and s m, n, m ≥ N is bounded above by b N
and b converges to zero, then s is a Cauchy sequence.
A Cauchy sequence on the natural numbers is bounded.
Yet another metric characterization of Cauchy sequences on integers. This one is often the most efficient.
def
pseudo_metric_space.induced
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(m : pseudo_metric_space β) :
Pseudometric space structure pulled back by a function.
Equations
- pseudo_metric_space.induced f m = {to_has_dist := {dist := λ (x y : α), has_dist.dist (f x) (f y)}, dist_self := _, dist_comm := _, dist_triangle := _, edist := λ (x y : α), has_edist.edist (f x) (f y), edist_dist := _, to_uniform_space := uniform_space.comap f pseudo_metric_space.to_uniform_space, uniformity_dist := _, to_bornology := bornology.induced f, cobounded_sets := _}
def
inducing.comap_pseudo_metric_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[pseudo_metric_space β]
{f : α → β}
(hf : inducing f) :
Pull back a pseudometric space structure by an inducing map. This is a version of
pseudo_metric_space.induced useful in case if the domain already has a topological_space
structure.
Equations
- hf.comap_pseudo_metric_space = (pseudo_metric_space.induced f _inst_3).replace_topology _
def
uniform_inducing.comap_pseudo_metric_space
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[pseudo_metric_space β]
(f : α → β)
(h : uniform_inducing f) :
Pull back a pseudometric space structure by a uniform inducing map. This is a version of
pseudo_metric_space.induced useful in case if the domain already has a uniform_space
structure.
Equations
@[protected, instance]
Equations
theorem
subtype.dist_eq
{α : Type u}
[pseudo_metric_space α]
{p : α → Prop}
(x y : subtype p) :
has_dist.dist x y = has_dist.dist ↑x ↑y
theorem
subtype.nndist_eq
{α : Type u}
[pseudo_metric_space α]
{p : α → Prop}
(x y : subtype p) :
has_nndist.nndist x y = has_nndist.nndist ↑x ↑y
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem
mul_opposite.dist_unop
{α : Type u}
[pseudo_metric_space α]
(x y : αᵐᵒᵖ) :
has_dist.dist (mul_opposite.unop x) (mul_opposite.unop y) = has_dist.dist x y
@[simp]
theorem
add_opposite.dist_unop
{α : Type u}
[pseudo_metric_space α]
(x y : αᵃᵒᵖ) :
has_dist.dist (add_opposite.unop x) (add_opposite.unop y) = has_dist.dist x y
@[simp]
theorem
mul_opposite.dist_op
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
has_dist.dist (mul_opposite.op x) (mul_opposite.op y) = has_dist.dist x y
@[simp]
theorem
add_opposite.dist_op
{α : Type u}
[pseudo_metric_space α]
(x y : α) :
has_dist.dist (add_opposite.op x) (add_opposite.op y) = has_dist.dist x y
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
@[protected, instance]
Equations
theorem
ulift.dist_eq
{β : Type v}
[pseudo_metric_space β]
(x y : ulift β) :
has_dist.dist x y = has_dist.dist x.down y.down
theorem
ulift.nndist_eq
{β : Type v}
[pseudo_metric_space β]
(x y : ulift β) :
has_nndist.nndist x y = has_nndist.nndist x.down y.down
@[simp]
theorem
ulift.dist_up_up
{β : Type v}
[pseudo_metric_space β]
(x y : β) :
has_dist.dist {down := x} {down := y} = has_dist.dist x y
@[simp]
theorem
ulift.nndist_up_up
{β : Type v}
[pseudo_metric_space β]
(x y : β) :
has_nndist.nndist {down := x} {down := y} = has_nndist.nndist x y
@[protected, instance]
def
prod.pseudo_metric_space_max
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β] :
pseudo_metric_space (α × β)
Equations
- prod.pseudo_metric_space_max = (pseudo_emetric_space.to_pseudo_metric_space_of_dist (λ (x y : α × β), has_dist.dist x.fst y.fst ⊔ has_dist.dist x.snd y.snd) prod.pseudo_metric_space_max._proof_1 prod.pseudo_metric_space_max._proof_2).replace_bornology prod.pseudo_metric_space_max._proof_3
theorem
prod.dist_eq
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{x y : α × β} :
has_dist.dist x y = linear_order.max (has_dist.dist x.fst y.fst) (has_dist.dist x.snd y.snd)
@[simp]
theorem
dist_prod_same_left
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{x : α}
{y₁ y₂ : β} :
has_dist.dist (x, y₁) (x, y₂) = has_dist.dist y₁ y₂
@[simp]
theorem
dist_prod_same_right
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{x₁ x₂ : α}
{y : β} :
has_dist.dist (x₁, y) (x₂, y) = has_dist.dist x₁ x₂
theorem
ball_prod_same
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(x : α)
(y : β)
(r : ℝ) :
metric.ball x r ×ˢ metric.ball y r = metric.ball (x, y) r
theorem
closed_ball_prod_same
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(x : α)
(y : β)
(r : ℝ) :
metric.closed_ball x r ×ˢ metric.closed_ball y r = metric.closed_ball (x, y) r
theorem
sphere_prod
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
(x : α × β)
(r : ℝ) :
metric.sphere x r = metric.sphere x.fst r ×ˢ metric.closed_ball x.snd r ∪ metric.closed_ball x.fst r ×ˢ metric.sphere x.snd r
theorem
uniform_continuous_dist
{α : Type u}
[pseudo_metric_space α] :
uniform_continuous (λ (p : α × α), has_dist.dist p.fst p.snd)
theorem
uniform_continuous.dist
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[uniform_space β]
{f g : β → α}
(hf : uniform_continuous f)
(hg : uniform_continuous g) :
uniform_continuous (λ (b : β), has_dist.dist (f b) (g b))
@[continuity]
theorem
continuous_dist
{α : Type u}
[pseudo_metric_space α] :
continuous (λ (p : α × α), has_dist.dist p.fst p.snd)
@[continuity]
theorem
continuous.dist
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{f g : β → α}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (b : β), has_dist.dist (f b) (g b))
theorem
filter.tendsto.dist
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f g : β → α}
{x : filter β}
{a b : α}
(hf : filter.tendsto f x (nhds a))
(hg : filter.tendsto g x (nhds b)) :
filter.tendsto (λ (x : β), has_dist.dist (f x) (g x)) x (nhds (has_dist.dist a b))
theorem
nhds_comap_dist
{α : Type u}
[pseudo_metric_space α]
(a : α) :
filter.comap (λ (a' : α), has_dist.dist a' a) (nhds 0) = nhds a
theorem
tendsto_iff_dist_tendsto_zero
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f : β → α}
{x : filter β}
{a : α} :
filter.tendsto f x (nhds a) ↔ filter.tendsto (λ (b : β), has_dist.dist (f b) a) x (nhds 0)
theorem
continuous_iff_continuous_dist
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{f : β → α} :
continuous f ↔ continuous (λ (x : β × β), has_dist.dist (f x.fst) (f x.snd))
theorem
uniform_continuous_nndist
{α : Type u}
[pseudo_metric_space α] :
uniform_continuous (λ (p : α × α), has_nndist.nndist p.fst p.snd)
theorem
uniform_continuous.nndist
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[uniform_space β]
{f g : β → α}
(hf : uniform_continuous f)
(hg : uniform_continuous g) :
uniform_continuous (λ (b : β), has_nndist.nndist (f b) (g b))
theorem
continuous_nndist
{α : Type u}
[pseudo_metric_space α] :
continuous (λ (p : α × α), has_nndist.nndist p.fst p.snd)
theorem
continuous.nndist
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{f g : β → α}
(hf : continuous f)
(hg : continuous g) :
continuous (λ (b : β), has_nndist.nndist (f b) (g b))
theorem
filter.tendsto.nndist
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f g : β → α}
{x : filter β}
{a b : α}
(hf : filter.tendsto f x (nhds a))
(hg : filter.tendsto g x (nhds b)) :
filter.tendsto (λ (x : β), has_nndist.nndist (f x) (g x)) x (nhds (has_nndist.nndist a b))
theorem
metric.is_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
is_closed (metric.closed_ball x ε)
theorem
metric.is_closed_sphere
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
is_closed (metric.sphere x ε)
@[simp]
theorem
metric.closure_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
closure (metric.closed_ball x ε) = metric.closed_ball x ε
@[simp]
theorem
metric.closure_sphere
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
closure (metric.sphere x ε) = metric.sphere x ε
theorem
metric.closure_ball_subset_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
closure (metric.ball x ε) ⊆ metric.closed_ball x ε
theorem
metric.frontier_ball_subset_sphere
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
frontier (metric.ball x ε) ⊆ metric.sphere x ε
theorem
metric.frontier_closed_ball_subset_sphere
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
frontier (metric.closed_ball x ε) ⊆ metric.sphere x ε
theorem
metric.ball_subset_interior_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{ε : ℝ} :
metric.ball x ε ⊆ interior (metric.closed_ball x ε)
theorem
metric.closed_ball_zero'
{α : Type u}
[pseudo_metric_space α]
(x : α) :
metric.closed_ball x 0 = closure {x}
theorem
metric.dense_range_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f : β → α} :
dense_range f ↔ ∀ (x : α) (r : ℝ), r > 0 → (∃ (y : β), has_dist.dist x (f y) < r)
theorem
topological_space.is_separable.separable_space
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(hs : topological_space.is_separable s) :
If a set s is separable, then the corresponding subtype is separable in a metric space.
This is not obvious, as the countable set whose closure covers s does not need in general to
be contained in s.
@[protected]
theorem
inducing.is_separable_preimage
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f : β → α}
[topological_space β]
(hf : inducing f)
{s : set α}
(hs : topological_space.is_separable s) :
The preimage of a separable set by an inducing map is separable.
@[protected]
theorem
embedding.is_separable_preimage
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f : β → α}
[topological_space β]
(hf : embedding f)
{s : set α}
(hs : topological_space.is_separable s) :
theorem
continuous_on.is_separable_image
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{f : α → β}
{s : set α}
(hf : continuous_on f s)
(hs : topological_space.is_separable s) :
If a map is continuous on a separable set s, then the image of s is also separable.
@[protected, instance]
def
pseudo_metric_space_pi
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)] :
pseudo_metric_space (Π (b : β), π b)
A finite product of pseudometric spaces is a pseudometric space, with the sup distance.
Equations
- pseudo_metric_space_pi = (pseudo_emetric_space.to_pseudo_metric_space_of_dist (λ (f g : Π (b : β), π b), ↑(finset.univ.sup (λ (b : β), has_nndist.nndist (f b) (g b)))) pseudo_metric_space_pi._proof_1 pseudo_metric_space_pi._proof_2).replace_bornology pseudo_metric_space_pi._proof_3
theorem
nndist_pi_def
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
(f g : Π (b : β), π b) :
has_nndist.nndist f g = finset.univ.sup (λ (b : β), has_nndist.nndist (f b) (g b))
theorem
dist_pi_def
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
(f g : Π (b : β), π b) :
has_dist.dist f g = ↑(finset.univ.sup (λ (b : β), has_nndist.nndist (f b) (g b)))
theorem
nndist_pi_le_iff
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
{f g : Π (b : β), π b}
{r : nnreal} :
has_nndist.nndist f g ≤ r ↔ ∀ (b : β), has_nndist.nndist (f b) (g b) ≤ r
theorem
nndist_pi_lt_iff
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
{f g : Π (b : β), π b}
{r : nnreal}
(hr : 0 < r) :
has_nndist.nndist f g < r ↔ ∀ (b : β), has_nndist.nndist (f b) (g b) < r
theorem
nndist_pi_eq_iff
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
{f g : Π (b : β), π b}
{r : nnreal}
(hr : 0 < r) :
has_nndist.nndist f g = r ↔ (∃ (i : β), has_nndist.nndist (f i) (g i) = r) ∧ ∀ (b : β), has_nndist.nndist (f b) (g b) ≤ r
theorem
dist_pi_lt_iff
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
{f g : Π (b : β), π b}
{r : ℝ}
(hr : 0 < r) :
has_dist.dist f g < r ↔ ∀ (b : β), has_dist.dist (f b) (g b) < r
theorem
dist_pi_le_iff
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
{f g : Π (b : β), π b}
{r : ℝ}
(hr : 0 ≤ r) :
has_dist.dist f g ≤ r ↔ ∀ (b : β), has_dist.dist (f b) (g b) ≤ r
theorem
dist_pi_eq_iff
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
{f g : Π (b : β), π b}
{r : ℝ}
(hr : 0 < r) :
has_dist.dist f g = r ↔ (∃ (i : β), has_dist.dist (f i) (g i) = r) ∧ ∀ (b : β), has_dist.dist (f b) (g b) ≤ r
theorem
dist_pi_le_iff'
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
[nonempty β]
{f g : Π (b : β), π b}
{r : ℝ} :
has_dist.dist f g ≤ r ↔ ∀ (b : β), has_dist.dist (f b) (g b) ≤ r
theorem
dist_pi_const_le
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[fintype β]
(a b : α) :
has_dist.dist (λ (_x : β), a) (λ (_x : β), b) ≤ has_dist.dist a b
theorem
nndist_pi_const_le
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[fintype β]
(a b : α) :
has_nndist.nndist (λ (_x : β), a) (λ (_x : β), b) ≤ has_nndist.nndist a b
@[simp]
theorem
dist_pi_const
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[fintype β]
[nonempty β]
(a b : α) :
has_dist.dist (λ (x : β), a) (λ (_x : β), b) = has_dist.dist a b
@[simp]
theorem
nndist_pi_const
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[fintype β]
[nonempty β]
(a b : α) :
has_nndist.nndist (λ (x : β), a) (λ (_x : β), b) = has_nndist.nndist a b
theorem
nndist_le_pi_nndist
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
(f g : Π (b : β), π b)
(b : β) :
has_nndist.nndist (f b) (g b) ≤ has_nndist.nndist f g
theorem
dist_le_pi_dist
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
(f g : Π (b : β), π b)
(b : β) :
has_dist.dist (f b) (g b) ≤ has_dist.dist f g
theorem
ball_pi
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
(x : Π (b : β), π b)
{r : ℝ}
(hr : 0 < r) :
metric.ball x r = set.univ.pi (λ (b : β), metric.ball (x b) r)
An open ball in a product space is a product of open balls. See also metric.ball_pi'
for a version assuming nonempty β instead of 0 < r.
theorem
ball_pi'
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
[nonempty β]
(x : Π (b : β), π b)
(r : ℝ) :
metric.ball x r = set.univ.pi (λ (b : β), metric.ball (x b) r)
An open ball in a product space is a product of open balls. See also metric.ball_pi
for a version assuming 0 < r instead of nonempty β.
theorem
closed_ball_pi
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
(x : Π (b : β), π b)
{r : ℝ}
(hr : 0 ≤ r) :
metric.closed_ball x r = set.univ.pi (λ (b : β), metric.closed_ball (x b) r)
A closed ball in a product space is a product of closed balls. See also metric.closed_ball_pi'
for a version assuming nonempty β instead of 0 ≤ r.
theorem
closed_ball_pi'
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
[nonempty β]
(x : Π (b : β), π b)
(r : ℝ) :
metric.closed_ball x r = set.univ.pi (λ (b : β), metric.closed_ball (x b) r)
A closed ball in a product space is a product of closed balls. See also metric.closed_ball_pi
for a version assuming 0 ≤ r instead of nonempty β.
theorem
sphere_pi
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
(x : Π (b : β), π b)
{r : ℝ}
(h : 0 < r ∨ nonempty β) :
metric.sphere x r = (⋃ (i : β), function.eval i ⁻¹' metric.sphere (x i) r) ∩ metric.closed_ball x r
A sphere in a product space is a union of spheres on each component restricted to the closed ball.
@[simp]
theorem
fin.nndist_insert_nth_insert_nth
{n : ℕ}
{α : fin (n + 1) → Type u_1}
[Π (i : fin (n + 1)), pseudo_metric_space (α i)]
(i : fin (n + 1))
(x y : α i)
(f g : Π (j : fin n), α (⇑(i.succ_above) j)) :
has_nndist.nndist (i.insert_nth x f) (i.insert_nth y g) = linear_order.max (has_nndist.nndist x y) (has_nndist.nndist f g)
@[simp]
theorem
fin.dist_insert_nth_insert_nth
{n : ℕ}
{α : fin (n + 1) → Type u_1}
[Π (i : fin (n + 1)), pseudo_metric_space (α i)]
(i : fin (n + 1))
(x y : α i)
(f g : Π (j : fin n), α (⇑(i.succ_above) j)) :
has_dist.dist (i.insert_nth x f) (i.insert_nth y g) = linear_order.max (has_dist.dist x y) (has_dist.dist f g)
theorem
real.dist_le_of_mem_pi_Icc
{β : Type v}
[fintype β]
{x y x' y' : β → ℝ}
(hx : x ∈ set.Icc x' y')
(hy : y ∈ set.Icc x' y') :
has_dist.dist x y ≤ has_dist.dist x' y'
theorem
finite_cover_balls_of_compact
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(hs : is_compact s)
{e : ℝ}
(he : 0 < e) :
Any compact set in a pseudometric space can be covered by finitely many balls of a given positive radius
theorem
is_compact.finite_cover_balls
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(hs : is_compact s)
{e : ℝ}
(he : 0 < e) :
Alias of finite_cover_balls_of_compact.
@[class]
- is_compact_closed_ball : ∀ (x : α) (r : ℝ), is_compact (metric.closed_ball x r)
A pseudometric space is proper if all closed balls are compact.
Instances of this typeclass
theorem
is_compact_sphere
{α : Type u_1}
[pseudo_metric_space α]
[proper_space α]
(x : α)
(r : ℝ) :
is_compact (metric.sphere x r)
In a proper pseudometric space, all spheres are compact.
@[protected, instance]
def
metric.sphere.compact_space
{α : Type u_1}
[pseudo_metric_space α]
[proper_space α]
(x : α)
(r : ℝ) :
compact_space ↥(metric.sphere x r)
In a proper pseudometric space, any sphere is a compact_space when considered as a subtype.
@[protected, instance]
A proper pseudo metric space is sigma compact, and therefore second countable.
theorem
tendsto_dist_right_cocompact_at_top
{α : Type u}
[pseudo_metric_space α]
[proper_space α]
(x : α) :
filter.tendsto (λ (y : α), has_dist.dist y x) (filter.cocompact α) filter.at_top
theorem
tendsto_dist_left_cocompact_at_top
{α : Type u}
[pseudo_metric_space α]
[proper_space α]
(x : α) :
theorem
proper_space_of_compact_closed_ball_of_le
{α : Type u}
[pseudo_metric_space α]
(R : ℝ)
(h : ∀ (x : α) (r : ℝ), R ≤ r → is_compact (metric.closed_ball x r)) :
If all closed balls of large enough radius are compact, then the space is proper. Especially useful when the lower bound for the radius is 0.
@[protected, instance]
@[protected, instance]
A proper space is locally compact
@[protected, instance]
A proper space is complete
@[protected, instance]
def
prod_proper_space
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
[proper_space α]
[proper_space β] :
proper_space (α × β)
A binary product of proper spaces is proper.
@[protected, instance]
def
pi_proper_space
{β : Type v}
{π : β → Type u_1}
[fintype β]
[Π (b : β), pseudo_metric_space (π b)]
[h : ∀ (b : β), proper_space (π b)] :
proper_space (Π (b : β), π b)
A finite product of proper spaces is proper.
theorem
exists_pos_lt_subset_ball
{α : Type u}
[pseudo_metric_space α]
[proper_space α]
{x : α}
{r : ℝ}
{s : set α}
(hr : 0 < r)
(hs : is_closed s)
(h : s ⊆ metric.ball x r) :
If a nonempty ball in a proper space includes a closed set s, then there exists a nonempty
ball with the same center and a strictly smaller radius that includes s.
theorem
exists_lt_subset_ball
{α : Type u}
[pseudo_metric_space α]
[proper_space α]
{x : α}
{r : ℝ}
{s : set α}
(hs : is_closed s)
(h : s ⊆ metric.ball x r) :
If a ball in a proper space includes a closed set s, then there exists a ball with the same
center and a strictly smaller radius that includes s.
theorem
is_compact.is_separable
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(hs : is_compact s) :
theorem
metric.second_countable_of_almost_dense_set
{α : Type u}
[pseudo_metric_space α]
(H : ∀ (ε : ℝ), ε > 0 → (∃ (s : set α), s.countable ∧ ∀ (x : α), ∃ (y : α) (H : y ∈ s), has_dist.dist x y ≤ ε)) :
A pseudometric space is second countable if, for every ε > 0, there is a countable set which
is ε-dense.
Boundedness of a subset of a pseudometric space. We formulate the definition to work even in the empty space.
theorem
metric.nonempty_of_unbounded
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(h : ¬metric.bounded s) :
s.nonempty
theorem
metric.bounded_iff_mem_bounded
{α : Type u}
[pseudo_metric_space α]
{s : set α} :
metric.bounded s ↔ ∀ (x : α), x ∈ s → metric.bounded s
Subsets of a bounded set are also bounded
Closed balls are bounded
theorem
metric.bounded_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{r : ℝ} :
metric.bounded (metric.ball x r)
Open balls are bounded
theorem
metric.bounded_sphere
{α : Type u}
[pseudo_metric_space α]
{x : α}
{r : ℝ} :
metric.bounded (metric.sphere x r)
Spheres are bounded
theorem
metric.bounded_iff_subset_ball
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(c : α) :
metric.bounded s ↔ ∃ (r : ℝ), s ⊆ metric.closed_ball c r
Given a point, a bounded subset is included in some ball around this point
theorem
metric.bounded.subset_ball
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(h : metric.bounded s)
(c : α) :
∃ (r : ℝ), s ⊆ metric.closed_ball c r
theorem
metric.bounded.subset_ball_lt
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(h : metric.bounded s)
(a : ℝ)
(c : α) :
theorem
metric.bounded_closure_of_bounded
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(h : metric.bounded s) :
theorem
metric.bounded.closure
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(h : metric.bounded s) :
Alias of metric.bounded_closure_of_bounded.
@[simp]
theorem
metric.bounded_closure_iff
{α : Type u}
[pseudo_metric_space α]
{s : set α} :
metric.bounded (closure s) ↔ metric.bounded s
theorem
metric.bounded.union
{α : Type u}
[pseudo_metric_space α]
{s t : set α}
(hs : metric.bounded s)
(ht : metric.bounded t) :
metric.bounded (s ∪ t)
The union of two bounded sets is bounded.
@[simp]
theorem
metric.bounded_union
{α : Type u}
[pseudo_metric_space α]
{s t : set α} :
metric.bounded (s ∪ t) ↔ metric.bounded s ∧ metric.bounded t
The union of two sets is bounded iff each of the sets is bounded.
theorem
metric.bounded_bUnion
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{I : set β}
{s : β → set α}
(H : I.finite) :
metric.bounded (⋃ (i : β) (H : i ∈ I), s i) ↔ ∀ (i : β), i ∈ I → metric.bounded (s i)
A finite union of bounded sets is bounded
@[protected]
theorem
metric.bounded.prod
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{s : set α}
{t : set β}
(hs : metric.bounded s)
(ht : metric.bounded t) :
metric.bounded (s ×ˢ t)
theorem
totally_bounded.bounded
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(h : totally_bounded s) :
A totally bounded set is bounded
A compact set is bounded
A finite set is bounded
Alias of metric.bounded_of_finite.
A singleton is bounded
theorem
metric.bounded_range_iff
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f : β → α} :
metric.bounded (set.range f) ↔ ∃ (C : ℝ), ∀ (x y : β), has_dist.dist (f x) (f y) ≤ C
Characterization of the boundedness of the range of a function
theorem
metric.bounded_range_of_tendsto_cofinite_uniformity
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f : β → α}
(hf : filter.tendsto (prod.map f f) (filter.cofinite.prod filter.cofinite) (uniformity α)) :
theorem
metric.bounded_range_of_cauchy_map_cofinite
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f : β → α}
(hf : cauchy (filter.map f filter.cofinite)) :
theorem
cauchy_seq.bounded_range
{α : Type u}
[pseudo_metric_space α]
{f : ℕ → α}
(hf : cauchy_seq f) :
theorem
metric.bounded_range_of_tendsto_cofinite
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f : β → α}
{a : α}
(hf : filter.tendsto f filter.cofinite (nhds a)) :
theorem
metric.bounded_of_compact_space
{α : Type u}
[pseudo_metric_space α]
{s : set α}
[compact_space α] :
In a compact space, all sets are bounded
theorem
metric.bounded_range_of_tendsto
{α : Type u}
[pseudo_metric_space α]
(u : ℕ → α)
{x : α}
(hu : filter.tendsto u filter.at_top (nhds x)) :
theorem
metric.exists_is_open_bounded_image_inter_of_is_compact_of_forall_continuous_within_at
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{k s : set β}
{f : β → α}
(hk : is_compact k)
(hf : ∀ (x : β), x ∈ k → continuous_within_at f s x) :
If a function is continuous within a set s at every point of a compact set k, then it is
bounded on some open neighborhood of k in s.
theorem
metric.exists_is_open_bounded_image_of_is_compact_of_forall_continuous_at
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{k : set β}
{f : β → α}
(hk : is_compact k)
(hf : ∀ (x : β), x ∈ k → continuous_at f x) :
If a function is continuous at every point of a compact set k, then it is bounded on
some open neighborhood of k.
theorem
metric.exists_is_open_bounded_image_inter_of_is_compact_of_continuous_on
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{k s : set β}
{f : β → α}
(hk : is_compact k)
(hks : k ⊆ s)
(hf : continuous_on f s) :
If a function is continuous on a set s containing a compact set k, then it is bounded on
some open neighborhood of k in s.
theorem
metric.exists_is_open_bounded_image_of_is_compact_of_continuous_on
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[topological_space β]
{k s : set β}
{f : β → α}
(hk : is_compact k)
(hs : is_open s)
(hks : k ⊆ s)
(hf : continuous_on f s) :
If a function is continuous on a neighborhood of a compact set k, then it is bounded on
some open neighborhood of k.
theorem
metric.is_compact_of_is_closed_bounded
{α : Type u}
[pseudo_metric_space α]
{s : set α}
[proper_space α]
(hc : is_closed s)
(hb : metric.bounded s) :
The Heine–Borel theorem: In a proper space, a closed bounded set is compact.
theorem
metric.bounded.is_compact_closure
{α : Type u}
[pseudo_metric_space α]
{s : set α}
[proper_space α]
(h : metric.bounded s) :
is_compact (closure s)
The Heine–Borel theorem: In a proper space, the closure of a bounded set is compact.
theorem
metric.is_compact_iff_is_closed_bounded
{α : Type u}
[pseudo_metric_space α]
{s : set α}
[t2_space α]
[proper_space α] :
is_compact s ↔ is_closed s ∧ metric.bounded s
The Heine–Borel theorem: In a proper Hausdorff space, a set is compact if and only if it is closed and bounded.
theorem
metric.compact_space_iff_bounded_univ
{α : Type u}
[pseudo_metric_space α]
[proper_space α] :
theorem
metric.bounded_Icc
{α : Type u}
[pseudo_metric_space α]
[preorder α]
[compact_Icc_space α]
(a b : α) :
metric.bounded (set.Icc a b)
theorem
metric.bounded_Ico
{α : Type u}
[pseudo_metric_space α]
[preorder α]
[compact_Icc_space α]
(a b : α) :
metric.bounded (set.Ico a b)
theorem
metric.bounded_Ioc
{α : Type u}
[pseudo_metric_space α]
[preorder α]
[compact_Icc_space α]
(a b : α) :
metric.bounded (set.Ioc a b)
theorem
metric.bounded_Ioo
{α : Type u}
[pseudo_metric_space α]
[preorder α]
[compact_Icc_space α]
(a b : α) :
metric.bounded (set.Ioo a b)
theorem
metric.bounded_of_bdd_above_of_bdd_below
{α : Type u}
[pseudo_metric_space α]
[preorder α]
[compact_Icc_space α]
{s : set α}
(h₁ : bdd_above s)
(h₂ : bdd_below s) :
In a pseudo metric space with a conditionally complete linear order such that the order and the metric structure give the same topology, any order-bounded set is metric-bounded.
The diameter of a set in a metric space. To get controllable behavior even when the diameter should be infinite, we express it in terms of the emetric.diameter
Equations
- metric.diam s = (emetric.diam s).to_real
The diameter of a set is always nonnegative
theorem
metric.diam_subsingleton
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(hs : s.subsingleton) :
metric.diam s = 0
@[simp]
The empty set has zero diameter
@[simp]
A singleton has zero diameter
@[simp]
@[simp]
theorem
metric.diam_pair
{α : Type u}
[pseudo_metric_space α]
{x y : α} :
metric.diam {x, y} = has_dist.dist x y
theorem
metric.diam_triple
{α : Type u}
[pseudo_metric_space α]
{x y z : α} :
metric.diam {x, y, z} = linear_order.max (linear_order.max (has_dist.dist x y) (has_dist.dist x z)) (has_dist.dist y z)
theorem
metric.ediam_le_of_forall_dist_le
{α : Type u}
[pseudo_metric_space α]
{s : set α}
{C : ℝ}
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist x y ≤ C) :
If the distance between any two points in a set is bounded by some constant C,
then ennreal.of_real C bounds the emetric diameter of this set.
theorem
metric.diam_le_of_forall_dist_le
{α : Type u}
[pseudo_metric_space α]
{s : set α}
{C : ℝ}
(h₀ : 0 ≤ C)
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist x y ≤ C) :
metric.diam s ≤ C
If the distance between any two points in a set is bounded by some non-negative constant, this constant bounds the diameter.
theorem
metric.diam_le_of_forall_dist_le_of_nonempty
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(hs : s.nonempty)
{C : ℝ}
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist x y ≤ C) :
metric.diam s ≤ C
If the distance between any two points in a nonempty set is bounded by some constant, this constant bounds the diameter.
theorem
metric.dist_le_diam_of_mem'
{α : Type u}
[pseudo_metric_space α]
{s : set α}
{x y : α}
(h : emetric.diam s ≠ ⊤)
(hx : x ∈ s)
(hy : y ∈ s) :
has_dist.dist x y ≤ metric.diam s
The distance between two points in a set is controlled by the diameter of the set.
theorem
metric.bounded_iff_ediam_ne_top
{α : Type u}
[pseudo_metric_space α]
{s : set α} :
metric.bounded s ↔ emetric.diam s ≠ ⊤
Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.
theorem
metric.bounded.ediam_ne_top
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(h : metric.bounded s) :
emetric.diam s ≠ ⊤
theorem
metric.ediam_univ_eq_top_iff_noncompact
{α : Type u}
[pseudo_metric_space α]
[proper_space α] :
@[simp]
theorem
metric.ediam_univ_of_noncompact
{α : Type u}
[pseudo_metric_space α]
[proper_space α]
[noncompact_space α] :
@[simp]
theorem
metric.diam_univ_of_noncompact
{α : Type u}
[pseudo_metric_space α]
[proper_space α]
[noncompact_space α] :
theorem
metric.dist_le_diam_of_mem
{α : Type u}
[pseudo_metric_space α]
{s : set α}
{x y : α}
(h : metric.bounded s)
(hx : x ∈ s)
(hy : y ∈ s) :
has_dist.dist x y ≤ metric.diam s
The distance between two points in a set is controlled by the diameter of the set.
theorem
metric.ediam_of_unbounded
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(h : ¬metric.bounded s) :
emetric.diam s = ⊤
theorem
metric.diam_eq_zero_of_unbounded
{α : Type u}
[pseudo_metric_space α]
{s : set α}
(h : ¬metric.bounded s) :
metric.diam s = 0
An unbounded set has zero diameter. If you would prefer to get the value ∞, use emetric.diam.
This lemma makes it possible to avoid side conditions in some situations
theorem
metric.diam_mono
{α : Type u}
[pseudo_metric_space α]
{s t : set α}
(h : s ⊆ t)
(ht : metric.bounded t) :
metric.diam s ≤ metric.diam t
If s ⊆ t, then the diameter of s is bounded by that of t, provided t is bounded.
theorem
metric.diam_union
{α : Type u}
[pseudo_metric_space α]
{s : set α}
{x y : α}
{t : set α}
(xs : x ∈ s)
(yt : y ∈ t) :
metric.diam (s ∪ t) ≤ metric.diam s + has_dist.dist x y + metric.diam t
The diameter of a union is controlled by the sum of the diameters, and the distance between
any two points in each of the sets. This lemma is true without any side condition, since it is
obviously true if s ∪ t is unbounded.
theorem
metric.diam_union'
{α : Type u}
[pseudo_metric_space α]
{s t : set α}
(h : (s ∩ t).nonempty) :
metric.diam (s ∪ t) ≤ metric.diam s + metric.diam t
If two sets intersect, the diameter of the union is bounded by the sum of the diameters.
theorem
metric.diam_le_of_subset_closed_ball
{α : Type u}
[pseudo_metric_space α]
{s : set α}
{x : α}
{r : ℝ}
(hr : 0 ≤ r)
(h : s ⊆ metric.closed_ball x r) :
metric.diam s ≤ 2 * r
theorem
metric.diam_closed_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{r : ℝ}
(h : 0 ≤ r) :
metric.diam (metric.closed_ball x r) ≤ 2 * r
The diameter of a closed ball of radius r is at most 2 r.
theorem
metric.diam_ball
{α : Type u}
[pseudo_metric_space α]
{x : α}
{r : ℝ}
(h : 0 ≤ r) :
metric.diam (metric.ball x r) ≤ 2 * r
The diameter of a ball of radius r is at most 2 r.
theorem
is_complete.nonempty_Inter_of_nonempty_bInter
{α : Type u}
[pseudo_metric_space α]
{s : ℕ → set α}
(h0 : is_complete (s 0))
(hs : ∀ (n : ℕ), is_closed (s n))
(h's : ∀ (n : ℕ), metric.bounded (s n))
(h : ∀ (N : ℕ), (⋂ (n : ℕ) (H : n ≤ N), s n).nonempty)
(h' : filter.tendsto (λ (n : ℕ), metric.diam (s n)) filter.at_top (nhds 0)) :
If a family of complete sets with diameter tending to 0 is such that each finite intersection
is nonempty, then the total intersection is also nonempty.
theorem
metric.nonempty_Inter_of_nonempty_bInter
{α : Type u}
[pseudo_metric_space α]
[complete_space α]
{s : ℕ → set α}
(hs : ∀ (n : ℕ), is_closed (s n))
(h's : ∀ (n : ℕ), metric.bounded (s n))
(h : ∀ (N : ℕ), (⋂ (n : ℕ) (H : n ≤ N), s n).nonempty)
(h' : filter.tendsto (λ (n : ℕ), metric.diam (s n)) filter.at_top (nhds 0)) :
In a complete space, if a family of closed sets with diameter tending to 0 is such that each
finite intersection is nonempty, then the total intersection is also nonempty.
theorem
metric.exists_local_min_mem_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[proper_space α]
[topological_space β]
[conditionally_complete_linear_order β]
[order_topology β]
{f : α → β}
{a z : α}
{r : ℝ}
(hf : continuous_on f (metric.closed_ball a r))
(hz : z ∈ metric.closed_ball a r)
(hf1 : ∀ (z' : α), z' ∈ metric.sphere a r → f z < f z') :
∃ (z : α) (H : z ∈ metric.ball a r), is_local_min f z
theorem
comap_dist_right_at_top_le_cocompact
{α : Type u}
[pseudo_metric_space α]
(x : α) :
filter.comap (λ (y : α), has_dist.dist y x) filter.at_top ≤ filter.cocompact α
theorem
comap_dist_right_at_top_eq_cocompact
{α : Type u}
[pseudo_metric_space α]
[proper_space α]
(x : α) :
filter.comap (λ (y : α), has_dist.dist y x) filter.at_top = filter.cocompact α
theorem
comap_dist_left_at_top_eq_cocompact
{α : Type u}
[pseudo_metric_space α]
[proper_space α]
(x : α) :
theorem
tendsto_cocompact_of_tendsto_dist_comp_at_top
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
{f : β → α}
{l : filter β}
(x : α)
(h : filter.tendsto (λ (y : β), has_dist.dist (f y) x) l filter.at_top) :
filter.tendsto f l (filter.cocompact α)
@[class]
- to_pseudo_metric_space : pseudo_metric_space α
- eq_of_dist_eq_zero : ∀ {x y : α}, has_dist.dist x y = 0 → x = y
We now define metric_space, extending pseudo_metric_space.
Instances of this typeclass
- normed_add_group.to_metric_space
- normed_group.to_metric_space
- normed_add_comm_group.to_metric_space
- normed_comm_group.to_metric_space
- non_unital_normed_ring.to_metric_space
- normed_ring.to_metric_space
- normed_division_ring.to_metric_space
- normed_field.to_metric_space
- normed_ordered_add_group.to_metric_space
- normed_ordered_group.to_metric_space
- normed_linear_ordered_add_group.to_metric_space
- normed_linear_ordered_group.to_metric_space
- normed_linear_ordered_field.to_metric_space
- normed_add_comm_group_of_ring.to_metric_space
- subtype.metric_space
- mul_opposite.metric_space
- add_opposite.metric_space
- empty.metric_space
- punit.metric_space
- real.metric_space
- nnreal.metric_space
- ulift.metric_space
- prod.metric_space_max
- metric_space_pi
- uniform_space.separation_quotient.metric_space
- additive.metric_space
- multiplicative.metric_space
- order_dual.metric_space
- int.metric_space
- nat.metric_space
- rat.metric_space
- uniform_space.completion.metric_space
- pi_Lp.metric_space
Instances of other typeclasses for metric_space
- metric_space.has_sizeof_inst
@[ext]
theorem
metric_space.ext
{α : Type u_1}
{m m' : metric_space α}
(h : pseudo_metric_space.to_has_dist = pseudo_metric_space.to_has_dist) :
m = m'
Two metric space structures with the same distance coincide.
def
metric_space.of_dist_topology
{α : Type u}
[topological_space α]
(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 α), is_open s ↔ ∀ (x : α), x ∈ s → (∃ (ε : ℝ) (H : ε > 0), ∀ (y : α), dist x y < ε → y ∈ s))
(eq_of_dist_eq_zero : ∀ (x y : α), dist x y = 0 → x = y) :
Construct a metric space structure whose underlying topological space structure (definitionally) agrees which a pre-existing topology which is compatible with a given distance function.
Equations
- metric_space.of_dist_topology dist dist_self dist_comm dist_triangle H eq_of_dist_eq_zero = {to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist (pseudo_metric_space.of_dist_topology dist dist_self dist_comm dist_triangle H), dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist (pseudo_metric_space.of_dist_topology dist dist_self dist_comm dist_triangle H), edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space (pseudo_metric_space.of_dist_topology dist dist_self dist_comm dist_triangle H), uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology (pseudo_metric_space.of_dist_topology dist dist_self dist_comm dist_triangle H), cobounded_sets := _}, eq_of_dist_eq_zero := eq_of_dist_eq_zero}
@[simp]
@[simp]
@[simp]
@[simp]
theorem
eq_of_forall_dist_le
{γ : Type w}
[metric_space γ]
{x y : γ}
(h : ∀ (ε : ℝ), ε > 0 → has_dist.dist x y ≤ ε) :
x = y
theorem
eq_of_nndist_eq_zero
{γ : Type w}
[metric_space γ]
{x y : γ} :
has_nndist.nndist x y = 0 → x = y
Deduce the equality of points with the vanishing of the nonnegative distance
@[simp]
Characterize the equality of points with the vanishing of the nonnegative distance
@[simp]
@[simp]
theorem
metric.closed_ball_zero
{γ : Type w}
[metric_space γ]
{x : γ} :
metric.closed_ball x 0 = {x}
@[simp]
theorem
metric.subsingleton_closed_ball
{γ : Type w}
[metric_space γ]
(x : γ)
{r : ℝ}
(hr : r ≤ 0) :
theorem
metric.subsingleton_sphere
{γ : Type w}
[metric_space γ]
(x : γ)
{r : ℝ}
(hr : r ≤ 0) :
(metric.sphere x r).subsingleton
@[protected, instance]
theorem
metric.uniform_embedding_iff'
{β : Type v}
{γ : Type w}
[metric_space γ]
[metric_space β]
{f : γ → β} :
A map between metric spaces is a uniform embedding if and only if the distance between f x
and f y is controlled in terms of the distance between x and y and conversely.
If a pseudo_metric_space is a T₀ space, then it is a metric_space.
Equations
- metric_space.of_t0_pseudo_metric_space α = {to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist _inst_3, dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist _inst_3, edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space _inst_3, uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology _inst_3, cobounded_sets := _}, eq_of_dist_eq_zero := _}
@[protected, instance]
A metric space induces an emetric space
theorem
metric.is_closed_of_pairwise_le_dist
{γ : Type w}
[metric_space γ]
{s : set γ}
{ε : ℝ}
(hε : 0 < ε)
(hs : s.pairwise (λ (x y : γ), ε ≤ has_dist.dist x y)) :
theorem
metric.closed_embedding_of_pairwise_le_dist
{γ : Type w}
[metric_space γ]
{α : Type u_1}
[topological_space α]
[discrete_topology α]
{ε : ℝ}
(hε : 0 < ε)
{f : α → γ}
(hf : pairwise (λ (x y : α), ε ≤ has_dist.dist (f x) (f y))) :
theorem
metric.uniform_embedding_bot_of_pairwise_le_dist
{α : Type u}
[pseudo_metric_space α]
{β : Type u_1}
{ε : ℝ}
(hε : 0 < ε)
{f : β → α}
(hf : pairwise (λ (x y : β), ε ≤ has_dist.dist (f x) (f y))) :
If f : β → α sends any two distinct points to points at distance at least ε > 0, then
f is a uniform embedding with respect to the discrete uniformity on β.
def
metric_space.replace_uniformity
{γ : Type u_1}
[U : uniform_space γ]
(m : metric_space γ)
(H : uniformity γ = uniformity γ) :
Build a new metric 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].
Equations
- m.replace_uniformity H = {to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist (metric_space.to_pseudo_metric_space.replace_uniformity H), dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist (metric_space.to_pseudo_metric_space.replace_uniformity H), edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space (metric_space.to_pseudo_metric_space.replace_uniformity H), uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology (metric_space.to_pseudo_metric_space.replace_uniformity H), cobounded_sets := _}, eq_of_dist_eq_zero := _}
theorem
metric_space.replace_uniformity_eq
{γ : Type u_1}
[U : uniform_space γ]
(m : metric_space γ)
(H : uniformity γ = uniformity γ) :
m.replace_uniformity H = m
@[reducible]
def
metric_space.replace_topology
{γ : Type u_1}
[U : topological_space γ]
(m : metric_space γ)
(H : U = uniform_space.to_topological_space) :
Build a new 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].
Equations
- m.replace_topology H = m.replace_uniformity _
theorem
metric_space.replace_topology_eq
{γ : Type u_1}
[U : topological_space γ]
(m : metric_space γ)
(H : U = uniform_space.to_topological_space) :
m.replace_topology H = m
def
emetric_space.to_metric_space_of_dist
{α : Type u}
[e : emetric_space α]
(dist : α → α → ℝ)
(edist_ne_top : ∀ (x y : α), has_edist.edist x y ≠ ⊤)
(h : ∀ (x y : α), dist x y = (has_edist.edist x y).to_real) :
One gets a metric 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 metric space and the emetric 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.
Equations
- emetric_space.to_metric_space_of_dist dist edist_ne_top h = metric_space.of_t0_pseudo_metric_space α
def
emetric_space.to_metric_space
{α : Type u}
[emetric_space α]
(h : ∀ (x y : α), has_edist.edist x y ≠ ⊤) :
One gets a metric 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 metric space and the emetric space.
Equations
- emetric_space.to_metric_space h = emetric_space.to_metric_space_of_dist (λ (x y : α), (has_edist.edist x y).to_real) h emetric_space.to_metric_space._proof_1
def
metric_space.replace_bornology
{α : Type u_1}
[B : bornology α]
(m : metric_space α)
(H : ∀ (s : set α), bornology.is_bounded s ↔ bornology.is_bounded s) :
Build a new metric 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].
Equations
- m.replace_bornology H = {to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist (metric_space.to_pseudo_metric_space.replace_bornology H), dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist (metric_space.to_pseudo_metric_space.replace_bornology H), edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space (metric_space.to_pseudo_metric_space.replace_bornology H), uniformity_dist := _, to_bornology := B, cobounded_sets := _}, eq_of_dist_eq_zero := _}
theorem
metric_space.replace_bornology_eq
{α : Type u_1}
[m : metric_space α]
[B : bornology α]
(H : ∀ (s : set α), bornology.is_bounded s ↔ bornology.is_bounded s) :
m.replace_bornology H = m
def
metric_space.induced
{γ : Type u_1}
{β : Type u_2}
(f : γ → β)
(hf : function.injective f)
(m : metric_space β) :
Metric space structure pulled back by an injective function. Injectivity is necessary to
ensure that dist x y = 0 only if x = y.
Equations
- metric_space.induced f hf m = {to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist (pseudo_metric_space.induced f metric_space.to_pseudo_metric_space), dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist (pseudo_metric_space.induced f metric_space.to_pseudo_metric_space), edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space (pseudo_metric_space.induced f metric_space.to_pseudo_metric_space), uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology (pseudo_metric_space.induced f metric_space.to_pseudo_metric_space), cobounded_sets := _}, eq_of_dist_eq_zero := _}
@[reducible]
def
uniform_embedding.comap_metric_space
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[metric_space β]
(f : α → β)
(h : uniform_embedding f) :
Pull back a metric space structure by a uniform embedding. This is a version of
metric_space.induced useful in case if the domain already has a uniform_space structure.
Equations
- uniform_embedding.comap_metric_space f h = (metric_space.induced f _ _inst_4).replace_uniformity _
@[reducible]
def
embedding.comap_metric_space
{α : Type u_1}
{β : Type u_2}
[topological_space α]
[metric_space β]
(f : α → β)
(h : embedding f) :
Pull back a metric space structure by an embedding. This is a version of
metric_space.induced useful in case if the domain already has a topological_space structure.
Equations
- embedding.comap_metric_space f h = let _inst : uniform_space α := embedding.comap_uniform_space f h in uniform_embedding.comap_metric_space f _
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
- empty.metric_space = {to_pseudo_metric_space := {to_has_dist := {dist := λ (_x _x : empty), 0}, dist_self := empty.metric_space._proof_1, dist_comm := empty.metric_space._proof_2, dist_triangle := empty.metric_space._proof_3, edist := λ (_x _x : empty), 0, edist_dist := empty.metric_space._proof_4, to_uniform_space := empty.uniform_space, uniformity_dist := empty.metric_space._proof_5, to_bornology := bornology.of_dist (λ (_x _x : empty), 0) empty.metric_space._proof_6 empty.metric_space._proof_7 empty.metric_space._proof_8, cobounded_sets := empty.metric_space._proof_9}, eq_of_dist_eq_zero := empty.metric_space._proof_10}
@[protected, instance]
Equations
- punit.metric_space = {to_pseudo_metric_space := {to_has_dist := {dist := λ (_x _x : punit), 0}, dist_self := punit.metric_space._proof_1, dist_comm := punit.metric_space._proof_2, dist_triangle := punit.metric_space._proof_3, edist := λ (_x _x : punit), 0, edist_dist := punit.metric_space._proof_4, to_uniform_space := punit.uniform_space, uniformity_dist := punit.metric_space._proof_5, to_bornology := bornology.of_dist (λ (_x _x : punit), 0) punit.metric_space._proof_6 punit.metric_space._proof_7 punit.metric_space._proof_8, cobounded_sets := punit.metric_space._proof_9}, eq_of_dist_eq_zero := punit.metric_space._proof_10}
@[protected, instance]
Instantiate the reals as a metric space.
Equations
- real.metric_space = {to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist real.pseudo_metric_space, dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist real.pseudo_metric_space, edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space real.pseudo_metric_space, uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology real.pseudo_metric_space, cobounded_sets := _}, eq_of_dist_eq_zero := real.metric_space._proof_1}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def
prod.metric_space_max
{β : Type v}
{γ : Type w}
[metric_space γ]
[metric_space β] :
metric_space (γ × β)
Equations
- prod.metric_space_max = {to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist prod.pseudo_metric_space_max, dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist prod.pseudo_metric_space_max, edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space prod.pseudo_metric_space_max, uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology prod.pseudo_metric_space_max, cobounded_sets := _}, eq_of_dist_eq_zero := _}
@[protected, instance]
def
metric_space_pi
{β : Type v}
{π : β → Type u_3}
[fintype β]
[Π (b : β), metric_space (π b)] :
metric_space (Π (b : β), π b)
A finite product of metric spaces is a metric space, with the sup distance.
Equations
- metric_space_pi = {to_pseudo_metric_space := {to_has_dist := pseudo_metric_space.to_has_dist pseudo_metric_space_pi, dist_self := _, dist_comm := _, dist_triangle := _, edist := pseudo_metric_space.edist pseudo_metric_space_pi, edist_dist := _, to_uniform_space := pseudo_metric_space.to_uniform_space pseudo_metric_space_pi, uniformity_dist := _, to_bornology := pseudo_metric_space.to_bornology pseudo_metric_space_pi, cobounded_sets := _}, eq_of_dist_eq_zero := _}
theorem
metric.second_countable_of_countable_discretization
{α : Type u}
[metric_space α]
(H : ∀ (ε : ℝ), ε > 0 → (∃ (β : Type u_1) (_x : encodable β) (F : α → β), ∀ (x y : α), F x = F y → has_dist.dist x y ≤ ε)) :
A metric space is second countable if one can reconstruct up to any ε>0 any element of the
space from countably many data.
@[protected, instance]
Equations
- uniform_space.separation_quotient.has_dist = {dist := λ (p q : uniform_space.separation_quotient α), quotient.lift_on₂' p q has_dist.dist uniform_space.separation_quotient.has_dist._proof_1}
theorem
uniform_space.separation_quotient.dist_mk
{α : Type u}
[pseudo_metric_space α]
(p q : α) :
has_dist.dist (quot.mk setoid.r p) (quot.mk setoid.r q) = has_dist.dist p q
@[protected, instance]
Equations
- uniform_space.separation_quotient.metric_space = emetric_space.to_metric_space_of_dist has_dist.dist uniform_space.separation_quotient.metric_space._proof_1 uniform_space.separation_quotient.metric_space._proof_2
additive, multiplicative #
The distance on those type synonyms is inherited without change.
@[protected, instance]
Equations
- additive.has_dist = _inst_3
@[protected, instance]
Equations
- multiplicative.has_dist = _inst_3
@[simp]
theorem
dist_of_mul
{X : Type u_1}
[has_dist X]
(a b : X) :
has_dist.dist (⇑additive.of_mul a) (⇑additive.of_mul b) = has_dist.dist a b
@[simp]
@[simp]
theorem
dist_to_mul
{X : Type u_1}
[has_dist X]
(a b : additive X) :
has_dist.dist (⇑additive.to_mul a) (⇑additive.to_mul b) = has_dist.dist a b
@[simp]
@[protected, instance]
Equations
- additive.pseudo_metric_space = _inst_3
@[protected, instance]
Equations
- multiplicative.pseudo_metric_space = _inst_3
@[simp]
@[simp]
@[simp]
@[simp]
@[protected, instance]
Equations
- additive.metric_space = _inst_3
@[protected, instance]
Equations
- multiplicative.metric_space = _inst_3
@[protected, instance]
def
additive.proper_space
{X : Type u_1}
[pseudo_metric_space X]
[proper_space X] :
proper_space (additive X)
@[protected, instance]
Order dual #
The distance on this type synonym is inherited without change.
@[protected, instance]
Equations
- order_dual.has_dist = _inst_3
@[simp]
@[simp]
@[protected, instance]
Equations
- order_dual.pseudo_metric_space = _inst_3
@[simp]
@[simp]
@[protected, instance]
Equations
- order_dual.metric_space = _inst_3
@[protected, instance]