isClosed_Icc

Mathlib.Topology.Order.OrderClosed

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

English

The closed interval Icc(a,b) is a closed set in any order topology that is OrderClosed.

Русский

Замкнутость отрезка Icc(a,b) в любом порядке с OrderClosedTopology.

LaTeX

$$$\text{IsClosed}(Icc(a,b))$$$

Lean4

theorem isClosed_Icc {a b : α} : IsClosed (Icc a b) :=
  IsClosed.inter isClosed_Ici isClosed_Iic

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

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

Разделы

Аффилиация

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