cthickening_subset_iUnion_closedBall_of_lt

English

For a metric space, δ>0 and δ' with δ < δ', the δ-thickening of E is contained in the union over x∈E of closed balls of radius δ' centered at x.

Русский

При δ'>δ>0 уплотнение δE ⊆ ⋃_{x∈E} { closedBall(x,δ') }.

LaTeX

$$$\operatorname{cthickening}_{\delta} E \subseteq \bigcup_{x\in E} \overline{B}(x,δ')$ for 0<δ' and δ<δ'.$$

Lean4

theorem cthickening_subset_iUnion_closedBall_of_lt {α : Type*} [PseudoMetricSpace α] (E : Set α) {δ δ' : ℝ}
    (hδ₀ : 0 < δ') (hδδ' : δ < δ') : cthickening δ E ⊆ ⋃ x ∈ E, closedBall x δ' :=
  by
  refine (cthickening_subset_thickening' hδ₀ hδδ' E).trans fun x hx => ?_
  obtain ⟨y, hy₁, hy₂⟩ := mem_thickening_iff.mp hx
  exact mem_iUnion₂.mpr ⟨y, hy₁, hy₂.le⟩

Похожие утверждения