Ioi_top — Mathlib

English

Let α be a preorder with a top element. The principal upper set generated by the top element equals the top element of the lattice of upper sets of α.

Русский

Пусть α упорядочено и существует верхний элемент. Главная верхняя множество над верхним элементом равна верхнему элементу решетки верхних множеств над α.

LaTeX

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

Lean4

@[simp]
nonrec theorem Ioi_top [OrderTop α] : Ioi (⊤ : α) = ⊤ :=
  SetLike.coe_injective Ioi_top

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