closure_interior_eq_closure_of_nonempty_interior

English

If s is convex and its interior is nonempty, then the closure of interior(s) equals the closure of s.

Русский

Если S выпукло и interior(S) не пусто, то closure(int(S)) = closure(S).

LaTeX

$$$$\overline{\operatorname{Int}(s)} = \overline{s}.$$$$

Lean4

theorem closure_interior_eq_closure_of_nonempty_interior {s : Set E} (hs : Convex 𝕜 s) (hs' : (interior s).Nonempty) :
    closure (interior s) = closure s :=
  subset_antisymm (closure_mono interior_subset) fun _ h ↦
    closure_mono (hs.openSegment_interior_closure_subset_interior hs'.choose_spec h)
      (segment_subset_closure_openSegment (right_mem_segment ..))

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