of_cthickening_subset_self — Mathlib

English

If δ>0 and cthickening δ s ⊆ s, then s is clopen.

Русский

Если δ>0 и cthickening δ s ⊆ s, то s является открытым и замкнутым.

LaTeX

$$$\text{IsClopen}.of_cthickening_subset_self\; (δ>0)\ (cthickening δ s ⊆ s) : \text{IsClopen } s$$$

Lean4

theorem of_cthickening_subset_self {δ : ℝ} (hδ : 0 < δ) (hs : cthickening δ s ⊆ s) : IsClopen s :=
  .of_thickening_subset_self hδ <| (thickening_subset_cthickening δ s).trans hs

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