Ici_ne_top — Mathlib

English

For every element a in α, the principal upper set generated by a is not equal to the top element of the lattice of upper sets.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem Ici_ne_top : Ici a ≠ ⊤ :=
  SetLike.coe_ne_coe.1 nonempty_Ici.ne_empty

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