Ici_lt_top — Mathlib

English

For any element a, the principal upper set generated by a is strictly below the top element of the lattice of upper sets.

Русский

Для любого элемента a получаемое от a главное верхнее множество строго ниже верхнего элемента решетки верхних множеств.

LaTeX

$$$\mathrm{Ici}(a) < \top$$$

Lean4

@[simp]
theorem Ici_lt_top : Ici a < ⊤ :=
  lt_top_iff_ne_top.2 Ici_ne_top

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