Ioo_subset_closure_interior

Mathlib.Topology.Order.OrderClosed

URI: https://scilib.ai/kg/mathlib#Ioo_subset_closure_interior

English

Ioo(a,b) is contained in the closure of interior(Ioo(a,b)).

Русский

Ioo(a,b) ⊆ closure(interior(Ioo(a,b))).

LaTeX

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

Lean4

theorem Ioo_subset_closure_interior : Ioo a b ⊆ closure (interior (Ioo a b)) := by
  simp only [interior_Ioo, subset_closure]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru