thickening_subset_interior_cthickening

English

For any δ and E, thickening δ E is contained in the interior of cthickening δ E.

Русский

Для любых δ и E утолщение δ E содержится внутриInterior cthickening δ E.

LaTeX

$$thickening δ E ⊆ interior (cthickening δ E)$$

Lean4

theorem thickening_subset_interior_cthickening (δ : ℝ) (E : Set α) : thickening δ E ⊆ interior (cthickening δ E) :=
  (subset_interior_iff_isOpen.mpr isOpen_thickening).trans (interior_mono (thickening_subset_cthickening δ E))

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