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_closedBall {α : Type u_2} [PseudoMetricSpace α] {x : α} {ε : ℝ} : IsClosed (closedBall x ε)

@[deprecated Metric.isClosed_closedBall (since := "2025-02-11")]

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

Alias of Metric.isClosed_closedBall.

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

theorem Metric.biInter_gt_closedBall {α : Type u_2} [PseudoMetricSpace α] (x : α) (r : ℝ) : ⋂ (r' : ℝ), ⋂ (_ : r' > r), closedBall x r' = closedBall x r

theorem Metric.biInter_gt_ball {α : Type u_2} [PseudoMetricSpace α] (x : α) (r : ℝ) : ⋂ (r' : ℝ), ⋂ (_ : r' > r), ball x r' = closedBall x r

theorem Metric.biUnion_lt_ball {α : Type u_2} [PseudoMetricSpace α] (x : α) (r : ℝ) : ⋃ (r' : ℝ), ⋃ (_ : r' < r), ball x r' = ball x r

theorem Metric.biUnion_lt_closedBall {α : Type u_2} [PseudoMetricSpace α] (x : α) (r : ℝ) : ⋃ (r' : ℝ), ⋃ (_ : r' < r), closedBall x r' = ball x r

theorem lebesgue_number_lemma_of_metric {α : Type u_2} [PseudoMetricSpace α] {s : Set α} {ι : Sort u_3} {c : ι → Set α} (hs : IsCompact s) (hc₁ : ∀ (i : ι), IsOpen (c i)) (hc₂ : s ⊆ ⋃ (i : ι), c i) : ∃ δ > 0, ∀ x ∈ s, ∃ (i : ι), Metric.ball x δ ⊆ c i

theorem lebesgue_number_lemma_of_metric_sUnion {α : Type u_2} [PseudoMetricSpace α] {s : Set α} {c : Set (Set α)} (hs : IsCompact s) (hc₁ : ∀ t ∈ c, IsOpen t) (hc₂ : s ⊆ ⋃₀ c) : ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, Metric.ball x δ ⊆ t