Ioi_eq_top

Mathlib.Order.UpperLower.Principal

URI: https://scilib.ai/kg/mathlib#UpperSet.Ioi_eq_top

English

For an element a in a top-ordered set, Ioi(a) equals the top iff a equals the top element.

Русский

Для элемента a в топово упорядоченном множестве Ioi(a) равна top тогда, когда a = top.

LaTeX

$$$\mathrm{Ioi}(a) = \top \iff a = \top$$$

Lean4

@[simp]
theorem Ioi_eq_top [OrderTop α] {a : α} : Ioi a = ⊤ ↔ a = ⊤ := by simp [UpperSet.ext_iff]

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

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

Разделы

Аффилиация

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