closure_thickening — Mathlib

English

For δ>0 and any set s, closure(thickening δ s) = cthickening δ s.

Русский

Для δ>0 и любого множества s выполняется closure(thickening δ s) = cthickening δ s.

LaTeX

$$$$\forall s\subseteq E:\; \operatorname{closure}(\operatorname{thickening}(\delta, s)) = \operatorname{cthickening}(\delta, s), \quad \delta > 0.$$$$

Lean4

@[simp]
theorem closure_thickening (hδ : 0 < δ) (s : Set E) : closure (thickening δ s) = cthickening δ s := by
  rw [← cthickening_zero, cthickening_thickening le_rfl hδ, zero_add]

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