lowerClosure_interior_subset' — Mathlib

English

If s is a lower set and x in closure s, then there exists y with small ball around y contained in a ball around x and inside interior s.

Русский

Если s — нижнее множество и x ∈ closure(s), существует y с шаром вокруг y внутри шарa вокруг x и внутри interior(s).

LaTeX

$$$\exists y\; (\overline{B}(y, δ/4) \subseteq \overline{B}(x, δ)) \land (\overline{B}(y, δ/4) \subseteq interior(s))$$$

Lean4

@[to_additive lowerClosure_interior_subset]
theorem lowerClosure_interior_subset' (s : Set α) : (lowerClosure (interior s) : Set α) ⊆ interior (lowerClosure s) :=
  lowerClosure_min (interior_mono subset_lowerClosure) (lowerClosure s).lower.interior

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