frontier_Ici_subset

Mathlib.Topology.Order.OrderClosed

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

English

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

Русский

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

LaTeX

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

Lean4

theorem frontier_Ici_subset (a : α) : frontier (Ici a) ⊆ { a } :=
  frontier_Iic_subset (α := αᵒᵈ) _

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

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

Разделы

Аффилиация

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