eq_top_iff

Mathlib.Order.LatticeIntervals

URI: https://scilib.ai/kg/mathlib#Set.Iic.eq_top_iff

English

An element x of Iic(a) is the top element iff its α-value is a.

Русский

Элемент x из Iic(a) является верхним тогда и только тогда, когда его значение в α равно a.

LaTeX

$$$$x = \\top_{\\mathrm{Iic}(a)} \\iff x^{\\uparrow} = a.$$$$

Lean4

protected theorem eq_top_iff [Preorder α] {x : Iic a} : x = ⊤ ↔ (x : α) = a := by simp [Subtype.ext_iff]

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

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

Разделы

Аффилиация

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