closure_interior_Icc — Mathlib

English

If a ≠ b in a densely ordered space, the closure of the interior of the closed interval [a,b] is exactly [a,b].

Русский

Для a ≠ b в плотно упорядоченном пространстве замыкание interior([a,b]) равно [a,b].

LaTeX

$$$\overline{\operatorname{int}(\mathrm{Icc}(a,b))} = \mathrm{Icc}(a,b)$$$

Lean4

theorem closure_interior_Icc {a b : α} (h : a ≠ b) : closure (interior (Icc a b)) = Icc a b :=
  (closure_minimal interior_subset isClosed_Icc).antisymm <|
    calc
      Icc a b = closure (Ioo a b) := (closure_Ioo h).symm
      _ ⊆ closure (interior (Icc a b)) := closure_mono (interior_maximal Ioo_subset_Icc_self isOpen_Ioo)

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