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

instance instOrderTopologyReal : OrderTopology ℝ

Equations

• instOrderTopologyReal = ⋯

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 tendsto_closedBall_smallSets {α : Type u_2} [PseudoMetricSpace α] (x : α) : Filter.Tendsto (Metric.closedBall x) (nhds 0) (nhds x).smallSets

theorem Metric.isClosed_ball {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsClosed (Metric.closedBall x ε)

theorem Metric.isClosed_sphere {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsClosed (Metric.sphere x ε)

@[simp]

theorem Metric.closure_closedBall {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : closure (Metric.closedBall x ε) = Metric.closedBall x ε

@[simp]

theorem Metric.closure_sphere {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : closure (Metric.sphere x ε) = Metric.sphere x ε

theorem Metric.closure_ball_subset_closedBall {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : closure (Metric.ball x ε) ⊆ Metric.closedBall x ε

theorem Metric.frontier_ball_subset_sphere {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : frontier (Metric.ball x ε) ⊆ Metric.sphere x ε

theorem Metric.frontier_closedBall_subset_sphere {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : frontier (Metric.closedBall x ε) ⊆ Metric.sphere x ε

theorem Metric.closedBall_zero' {α : Type u_2} [PseudoMetricSpace α] (x : α) : Metric.closedBall x 0 = closure {x}

theorem Metric.eventually_isCompact_closedBall {α : Type u_2} [PseudoMetricSpace α] [WeaklyLocallyCompactSpace α] (x : α) : ∀ᶠ (r : ℝ) in nhds 0, IsCompact (Metric.closedBall x r)

theorem Metric.exists_isCompact_closedBall {α : Type u_2} [PseudoMetricSpace α] [WeaklyLocallyCompactSpace α] (x : α) : ∃ (r : ℝ), 0 < r ∧ IsCompact (Metric.closedBall x r)

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'