Ico_subset_closure_interior — Mathlib

English

Similarly, the half-open interval Ico(a,b) is contained in the closure of its interior.

Русский

Аналогично, полууточный интервал Ico(a,b) содержится в замыкании своей внутренности.

LaTeX

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

Lean4

theorem Ico_subset_closure_interior (a b : α) : Ico a b ⊆ closure (interior (Ico a b)) := by
  simpa only [Ioc_toDual] using Ioc_subset_closure_interior (OrderDual.toDual b) (OrderDual.toDual a)

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