Ioc_subset_closure_interior — Mathlib

English

For any a,b in a densely ordered space, the interval Ioc(a,b) is contained in the closure of its interior.

Русский

Для любых a,b в плотно упорядоченном пространстве Ioc(a,b) ⊆ замыкание внутренности Ioc(a,b).

LaTeX

$$$\mathrm{Ioc}(a,b) \subseteq \overline{\operatorname{int}(\mathrm{Ioc}(a,b))}$$$

Lean4

theorem Ioc_subset_closure_interior (a b : α) : Ioc a b ⊆ closure (interior (Ioc a b)) :=
  by
  rcases eq_or_ne a b with (rfl | h)
  · simp
  ·
    calc
      Ioc a b ⊆ Icc a b := Ioc_subset_Icc_self
      _ = closure (Ioo a b) := (closure_Ioo h).symm
      _ ⊆ closure (interior (Ioc a b)) := closure_mono (interior_maximal Ioo_subset_Ioc_self isOpen_Ioo)

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