Ici_bot — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{Ici}(\perp) = \perp$$$

Lean4

@[simp]
nonrec theorem Ici_bot [OrderBot α] : Ici (⊥ : α) = ⊥ :=
  SetLike.coe_injective Ici_bot

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