Extra lemmas about pseudo-metric spaces #
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)