cthickening_eq_biUnion_closedBall

English

If E is closed, then cthickening δ E equals the union over x ∈ E of closedBall x δ.

Русский

Если E замкнуто, то δ-уплотнение E равно объединению замкнутых шаров по x∈E радиуса δ.

LaTeX

$$$\operatorname{cthickening}_{\delta} E = \bigcup_{x∈E} \overline{B}(x,δ)$$$

Lean4

nonrec theorem _root_.IsClosed.cthickening_eq_biUnion_closedBall {α : Type*} [PseudoMetricSpace α] [ProperSpace α]
    {E : Set α} (hE : IsClosed E) (hδ : 0 ≤ δ) : cthickening δ E = ⋃ x ∈ E, closedBall x δ := by
  rw [cthickening_eq_biUnion_closedBall E hδ, hE.closure_eq]

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