Extra lemmas about pseudo-metric spaces

instance instOrderTopologyReal : OrderTopology ℝ

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)