Ici_eq_Icc

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#Finset.Ici_eq_Icc

English

In a locally finite order with top, the set of elements > a equals the open-closed interval (a, ⊤].

Русский

В локально конечном порядке с верхой элементом множество > a равно интервалу (a, ⊤].

LaTeX

$$Ioi a = Ioc a ⊤$$

Lean4

theorem Ici_eq_Icc (a : α) : Ici a = Icc a ⊤ :=
  rfl

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

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

Разделы

Аффилиация

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