Mathlib.Topology.MetricSpace.Pseudo.Lemmas

instOrderTopologyReal instance

: OrderTopology ℝ

Full source

instance : OrderTopology ℝ :=
  orderTopology_of_nhds_abs fun x => by
    simp only [nhds_basis_ball.eq_biInf, ball, Real.dist_eq, abs_sub_comm]

Order Topology on Real Numbers

Informal description

The real numbers $\mathbb{R}$ are equipped with the order topology, which is generated by open intervals and coincides with the topology induced by the standard metric on $\mathbb{R}$.

Real.singleton_eq_inter_Icc theorem

(b : ℝ) : { b } = ⋂ (r > 0), Icc (b - r) (b + r)

Full source

lemma Real.singleton_eq_inter_Icc (b : ℝ) : {b} = ⋂ (r > 0), Icc (b - r) (b + r) := by
  simp [Icc_eq_closedBall, biInter_basis_nhds Metric.nhds_basis_closedBall]

Singleton as Intersection of Closed Intervals in Real Numbers

Informal description

For any real number $b$, the singleton set $\{b\}$ is equal to the intersection of all closed intervals $[b - r, b + r]$ for $r > 0$, i.e., \[ \{b\} = \bigcap_{r > 0} [b - r, b + r]. \]

squeeze_zero' theorem

 {α} {f g : α → ℝ} {t₀ : Filter α} (hf : ∀ᶠ t in t₀, 0 ≤ f t) (hft : ∀ᶠ t in t₀, f t ≤ g t) (g0 : Tendsto g t₀ (𝓝 0)) :
  Tendsto f t₀ (𝓝 0)

Full source

/-- Special case of the sandwich lemma; see `tendsto_of_tendsto_of_tendsto_of_le_of_le'` for the
general case. -/
lemma squeeze_zero' {α} {f g : α → ℝ} {t₀ : Filter α} (hf : ∀ᶠ t in t₀, 0 ≤ f t)
    (hft : ∀ᶠ t in t₀, f t ≤ g t) (g0 : Tendsto g t₀ (𝓝 0)) : Tendsto f t₀ (𝓝 0) :=
  tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds g0 hf hft

Squeeze Theorem for Functions Tending to Zero (Eventual Version)

Informal description

Let $f, g : \alpha \to \mathbb{R}$ be functions and $t_0$ be a filter on $\alpha$. Suppose that eventually $0 \leq f(t) \leq g(t)$ for all $t \in \alpha$, and that $g$ tends to $0$ along $t_0$. Then $f$ also tends to $0$ along $t_0$.

squeeze_zero theorem

 {α} {f g : α → ℝ} {t₀ : Filter α} (hf : ∀ t, 0 ≤ f t) (hft : ∀ t, f t ≤ g t) (g0 : Tendsto g t₀ (𝓝 0)) :
  Tendsto f t₀ (𝓝 0)

Full source

/-- 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. -/
lemma squeeze_zero {α} {f g : α → ℝ} {t₀ : Filter α} (hf : ∀ t, 0 ≤ f t) (hft : ∀ t, f t ≤ g t)
    (g0 : Tendsto g t₀ (𝓝 0)) : Tendsto f t₀ (𝓝 0) :=
  squeeze_zero' (Eventually.of_forall hf) (Eventually.of_forall hft) g0

Squeeze Theorem for Functions Tending to Zero (Uniform Version)

Informal description

Let $f, g : \alpha \to \mathbb{R}$ be functions and $t_0$ be a filter on $\alpha$. If for all $t \in \alpha$, $0 \leq f(t) \leq g(t)$, and $g$ tends to $0$ along $t_0$, then $f$ also tends to $0$ along $t_0$.

eventually_closedBall_subset theorem

{x : α} {u : Set α} (hu : u ∈ 𝓝 x) : ∀ᶠ r in 𝓝 (0 : ℝ), closedBall x r ⊆ u

Full source

/-- If `u` is a neighborhood of `x`, then for small enough `r`, the closed ball
`Metric.closedBall x r` is contained in `u`. -/
lemma eventually_closedBall_subset {x : α} {u : Set α} (hu : u ∈ 𝓝 x) :
    ∀ᶠ r in 𝓝 (0 : ℝ), closedBall x r ⊆ u := by
  obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu
  have : IicIic ε ∈ 𝓝 (0 : ℝ) := Iic_mem_nhds εpos
  filter_upwards [this] with _ hr using Subset.trans (closedBall_subset_closedBall hr) hε

Existence of Small Closed Balls Within Neighborhoods in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any neighborhood $u$ of $x$, there exists a sufficiently small radius $r > 0$ such that the closed ball $\overline{B}(x, r)$ is contained in $u$.

tendsto_closedBall_smallSets theorem

(x : α) : Tendsto (closedBall x) (𝓝 0) (𝓝 x).smallSets

Full source

lemma tendsto_closedBall_smallSets (x : α) : Tendsto (closedBall x) (𝓝 0) (𝓝 x).smallSets :=
  tendsto_smallSets_iff.2 fun _ ↦ eventually_closedBall_subset

Closed Balls Tend to Small Sets as Radius Tends to Zero

Informal description

For any point $x$ in a pseudometric space $\alpha$, the function mapping radii $r$ to closed balls $\overline{B}(x, r)$ tends to the small sets neighborhood filter of $x$ as $r$ tends to $0$.

Metric.isClosed_closedBall theorem

: IsClosed (closedBall x ε)

Full source

lemma isClosed_closedBall : IsClosed (closedBall x ε) :=
  isClosed_le (continuous_id.dist continuous_const) continuous_const

Closedness of Closed Balls in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the closed ball $\overline{B}(x, \varepsilon) = \{ y \in \alpha \mid \text{dist}(y, x) \leq \varepsilon \}$ is a closed set in the topology induced by the pseudometric.

Metric.isClosed_sphere theorem

: IsClosed (sphere x ε)

Full source

lemma isClosed_sphere : IsClosed (sphere x ε) :=
  isClosed_eq (continuous_id.dist continuous_const) continuous_const

Closedness of Spheres in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the sphere $\{y \in \alpha \mid \text{dist}(y, x) = \varepsilon\}$ is a closed set in $\alpha$.

Metric.closure_closedBall theorem

: closure (closedBall x ε) = closedBall x ε

Full source

@[simp]
lemma closure_closedBall : closure (closedBall x ε) = closedBall x ε :=
  isClosed_closedBall.closure_eq

Closure of Closed Ball Equals Itself in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the closure of the closed ball $\overline{B}(x, \varepsilon)$ is equal to itself, i.e., $\overline{\overline{B}(x, \varepsilon)} = \overline{B}(x, \varepsilon)$.

Metric.closure_sphere theorem

: closure (sphere x ε) = sphere x ε

Full source

@[simp]
lemma closure_sphere : closure (sphere x ε) = sphere x ε :=
  isClosed_sphere.closure_eq

Closure of Sphere Equals Itself in Pseudometric Spaces

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the closure of the sphere $\{y \in \alpha \mid \text{dist}(y, x) = \varepsilon\}$ is equal to the sphere itself, i.e., $\overline{\text{sphere}(x, \varepsilon)} = \text{sphere}(x, \varepsilon)$.

Metric.closure_ball_subset_closedBall theorem

: closure (ball x ε) ⊆ closedBall x ε

Full source

lemma closure_ball_subset_closedBall : closureclosure (ball x ε) ⊆ closedBall x ε :=
  closure_minimal ball_subset_closedBall isClosed_closedBall

Closure of Open Ball is Contained in Closed Ball

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon$, the closure of the open ball $B(x, \varepsilon)$ is contained in the closed ball $\overline{B}(x, \varepsilon)$. That is, $\overline{B(x, \varepsilon)} \subseteq \{ y \in \alpha \mid \text{dist}(y, x) \leq \varepsilon \}$.

Metric.frontier_ball_subset_sphere theorem

: frontier (ball x ε) ⊆ sphere x ε

Full source

lemma frontier_ball_subset_sphere : frontierfrontier (ball x ε) ⊆ sphere x ε :=
  frontier_lt_subset_eq (continuous_id.dist continuous_const) continuous_const

Frontier of Open Ball is Contained in Sphere

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any positive real number $\varepsilon$, the frontier of the open ball $\text{ball}(x, \varepsilon)$ is contained in the sphere $\text{sphere}(x, \varepsilon)$. That is, $\text{frontier}(\text{ball}(x, \varepsilon)) \subseteq \text{sphere}(x, \varepsilon)$.

Metric.frontier_closedBall_subset_sphere theorem

: frontier (closedBall x ε) ⊆ sphere x ε

Full source

lemma frontier_closedBall_subset_sphere : frontierfrontier (closedBall x ε) ⊆ sphere x ε :=
  frontier_le_subset_eq (continuous_id.dist continuous_const) continuous_const

Frontier of Closed Ball is Contained in Sphere

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any non-negative real number $\varepsilon$, the frontier of the closed ball $\overline{B}(x, \varepsilon)$ is contained in the sphere $\text{sphere}(x, \varepsilon)$. That is, $\text{frontier}(\overline{B}(x, \varepsilon)) \subseteq \{ y \in \alpha \mid \text{dist}(y, x) = \varepsilon \}$.

Metric.closedBall_zero' theorem

(x : α) : closedBall x 0 = closure { x }

Full source

lemma closedBall_zero' (x : α) : closedBall x 0 = closure {x} :=
  Subset.antisymm
    (fun _y hy =>
      mem_closure_iff.2 fun _ε ε0 => ⟨x, mem_singleton x, (mem_closedBall.1 hy).trans_lt ε0⟩)
    (closure_minimal (singleton_subset_iff.2 (dist_self x).le) isClosed_closedBall)

Closed Ball of Radius Zero Equals Closure of Singleton: $\overline{B}(x, 0) = \overline{\{x\}}$

Informal description

For any point $x$ in a pseudometric space $\alpha$, the closed ball centered at $x$ with radius $0$ is equal to the closure of the singleton set $\{x\}$, i.e., $\overline{B}(x, 0) = \overline{\{x\}}$.

Metric.eventually_isCompact_closedBall theorem

[WeaklyLocallyCompactSpace α] (x : α) : ∀ᶠ r in 𝓝 (0 : ℝ), IsCompact (closedBall x r)

Full source

lemma eventually_isCompact_closedBall [WeaklyLocallyCompactSpace α] (x : α) :
    ∀ᶠ r in 𝓝 (0 : ℝ), IsCompact (closedBall x r) := by
  rcases exists_compact_mem_nhds x with ⟨s, s_compact, hs⟩
  filter_upwards [eventually_closedBall_subset hs] with r hr
  exact IsCompact.of_isClosed_subset s_compact isClosed_closedBall hr

Existence of Small Compact Closed Balls in Weakly Locally Compact Pseudometric Spaces

Informal description

In a weakly locally compact pseudometric space $\alpha$, for any point $x \in \alpha$, there exists a neighborhood of $0$ in $\mathbb{R}$ such that for all radii $r$ in this neighborhood, the closed ball $\overline{B}(x, r)$ is compact.

Metric.exists_isCompact_closedBall theorem

[WeaklyLocallyCompactSpace α] (x : α) : ∃ r, 0 < r ∧ IsCompact (closedBall x r)

Full source

lemma exists_isCompact_closedBall [WeaklyLocallyCompactSpace α] (x : α) :
    ∃ r, 0 < r ∧ IsCompact (closedBall x r) := by
  have : ∀ᶠ r in 𝓝[>] 0, IsCompact (closedBall x r) :=
    eventually_nhdsWithin_of_eventually_nhds (eventually_isCompact_closedBall x)
  simpa only [and_comm] using (this.and self_mem_nhdsWithin).exists

Existence of Compact Closed Balls in Weakly Locally Compact Pseudometric Spaces

Informal description

In a weakly locally compact pseudometric space $\alpha$, for any point $x \in \alpha$, there exists a positive real number $r > 0$ such that the closed ball $\overline{B}(x, r)$ is compact.

Metric.biInter_gt_closedBall theorem

(x : α) (r : ℝ) : ⋂ r' > r, closedBall x r' = closedBall x r

Full source

theorem biInter_gt_closedBall (x : α) (r : ℝ) : ⋂ r' > r, closedBall x r' = closedBall x r := by
  ext
  simp [forall_gt_imp_ge_iff_le_of_dense]

Intersection of Closed Balls Greater Than Radius Equals Closed Ball

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $r$, the intersection of all closed balls $\overline{B}(x, r')$ with $r' > r$ is equal to the closed ball $\overline{B}(x, r)$. That is, \[ \bigcap_{r' > r} \overline{B}(x, r') = \overline{B}(x, r). \]

Metric.biInter_gt_ball theorem

(x : α) (r : ℝ) : ⋂ r' > r, ball x r' = closedBall x r

Full source

theorem biInter_gt_ball (x : α) (r : ℝ) : ⋂ r' > r, ball x r' = closedBall x r := by
  ext
  simp [forall_lt_iff_le']

Intersection of Larger Open Balls Equals Closed Ball

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $r$, the intersection of all open balls $B(x, r')$ with $r' > r$ is equal to the closed ball $\overline{B}(x, r)$. That is, \[ \bigcap_{r' > r} B(x, r') = \overline{B}(x, r). \]

Metric.biUnion_lt_ball theorem

(x : α) (r : ℝ) : ⋃ r' < r, ball x r' = ball x r

Full source

theorem biUnion_lt_ball (x : α) (r : ℝ) : ⋃ r' < r, ball x r' = ball x r := by
  ext
  rw [← not_iff_not]
  simp [forall_lt_imp_le_iff_le_of_dense]

Union of Smaller Balls Equals Ball

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $r$, the union of all open balls $B(x, r')$ with $r' < r$ is equal to the open ball $B(x, r)$. That is, \[ \bigcup_{r' < r} B(x, r') = B(x, r). \]

Metric.biUnion_lt_closedBall theorem

(x : α) (r : ℝ) : ⋃ r' < r, closedBall x r' = ball x r

Full source

theorem biUnion_lt_closedBall (x : α) (r : ℝ) : ⋃ r' < r, closedBall x r' = ball x r := by
  ext
  rw [← not_iff_not]
  simp [forall_lt_iff_le]

Union of Smaller Closed Balls Equals Open Ball

Informal description

For any point $x$ in a pseudometric space $\alpha$ and any real number $r$, the union of all closed balls $\overline{B}(x, r')$ with $r' < r$ is equal to the open ball $B(x, r)$. That is, \[ \bigcup_{r' < r} \overline{B}(x, r') = B(x, r). \]

lebesgue_number_lemma_of_metric theorem

 {s : Set α} {ι : Sort*} {c : ι → Set α} (hs : IsCompact s) (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i, c i) :
  ∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i

Full source

theorem lebesgue_number_lemma_of_metric {s : Set α} {ι : Sort*} {c : ι → Set α} (hs : IsCompact s)
    (hc₁ : ∀ i, IsOpen (c i)) (hc₂ : s ⊆ ⋃ i, c i) : ∃ δ > 0, ∀ x ∈ s, ∃ i, ball x δ ⊆ c i := by
  simpa only [ball, UniformSpace.ball, preimage_setOf_eq, dist_comm]
    using uniformity_basis_dist.lebesgue_number_lemma hs hc₁ hc₂

Lebesgue Number Lemma for Compact Sets in Pseudometric Spaces

Informal description

Let $s$ be a compact subset of a pseudometric space $\alpha$, and let $\{c_i\}_{i \in \iota}$ be a family of open subsets of $\alpha$ such that $s \subseteq \bigcup_{i} c_i$. Then there exists a positive real number $\delta > 0$ such that for every point $x \in s$, there exists an index $i$ for which the open ball $B(x, \delta)$ is entirely contained in $c_i$.

lebesgue_number_lemma_of_metric_sUnion theorem

 {s : Set α} {c : Set (Set α)} (hs : IsCompact s) (hc₁ : ∀ t ∈ c, IsOpen t) (hc₂ : s ⊆ ⋃₀ c) :
  ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t

Full source

theorem lebesgue_number_lemma_of_metric_sUnion {s : Set α} {c : Set (Set α)} (hs : IsCompact s)
    (hc₁ : ∀ t ∈ c, IsOpen t) (hc₂ : s ⊆ ⋃₀ c) : ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t := by
  rw [sUnion_eq_iUnion] at hc₂; simpa using lebesgue_number_lemma_of_metric hs (by simpa) hc₂

Lebesgue Number Lemma for Compact Sets with Set-Based Cover in Pseudometric Spaces

Informal description

Let $s$ be a compact subset of a pseudometric space $\alpha$, and let $c$ be a collection of open subsets of $\alpha$ such that $s$ is covered by the union of all sets in $c$, i.e., $s \subseteq \bigcup_{t \in c} t$. Then there exists a positive real number $\delta > 0$ such that for every point $x \in s$, there exists a set $t \in c$ for which the open ball $B(x, \delta)$ is entirely contained in $t$.