frontier_Iic_subset

Mathlib.Topology.Order.OrderClosed

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

English

The frontier of Iic(a) is contained in {a}.

Русский

Граница множества Iic(a) содержится в {a}.

LaTeX

$$$ \\text{frontier}(Iic(a)) \\subseteq \\{a\\}$$$

Lean4

theorem frontier_Iic_subset (a : α) : frontier (Iic a) ⊆ { a } :=
  frontier_le_subset_eq (@continuous_id α _) continuous_const

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

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

Разделы

Аффилиация

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