Documentation

Mathlib.Topology.MetricSpace.Pseudo.Lemmas

Extra lemmas about pseudo-metric spaces #

theorem Real.dist_left_le_of_mem_uIcc {x : } {y : } {z : } (h : y Set.uIcc x z) :
dist x y dist x z
theorem Real.dist_right_le_of_mem_uIcc {x : } {y : } {z : } (h : y Set.uIcc x z) :
dist y z 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') :
dist x y 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') :
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) :
dist x y 1
theorem Real.singleton_eq_inter_Icc (b : ) :
{b} = ⋂ (r : ), ⋂ (_ : r > 0), Set.Icc (b - r) (b + r)
theorem squeeze_zero' {α : Type u_3} {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 lemma; see tendsto_of_tendsto_of_tendsto_of_le_of_le' for the general case.

theorem squeeze_zero {α : Type u_3} {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 lemma; 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 eventually_closedBall_subset {α : Type u_2} [PseudoMetricSpace α] {x : α} {u : Set α} (hu : u nhds x) :
∀ᶠ (r : ) in nhds 0, Metric.closedBall x r u

If u is a neighborhood of x, then for small enough r, the closed ball Metric.closedBall x r is contained in u.

theorem Metric.isClosed_ball {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : } :
theorem Metric.isClosed_sphere {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : } :
@[simp]
@[simp]
theorem Metric.closure_sphere {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : } :
theorem Real.dist_le_of_mem_pi_Icc {ι : Type u_1} [Fintype ι] {x : ι} {y : ι} {x' : ι} {y' : ι} (hx : x Set.Icc x' y') (hy : y Set.Icc x' y') :
dist x y dist x' y'