interior_subset_closure — Mathlib

English

For any set s in a topological space X, the interior of s is contained in the closure of s: interior(s) ⊆ closure(s).

Русский

Для любого множества s в топологическом пространстве X внутренняя часть s содержится в его замыкании: int(s) ⊆ cl(s).

LaTeX

$$$\\\\operatorname{int}(s) \\\\subseteq \\\\overline{s}$$$

Lean4

theorem interior_subset_closure : interior s ⊆ closure s :=
  Subset.trans interior_subset subset_closure

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