bot_ne_top — Mathlib

English

In a nontrivial ordered set with a bounded order, the bottom and top are distinct: ⊥ ≠ ⊤.

Русский

В не тривиальном упорядоченном множестве с ограниченным порядком нижняя и верхняя границы различны: ⊥ ≠ ⊤.

LaTeX

$$$\\bot_{\\alpha} \\neq \\top_{\\alpha}$$$

Lean4

@[simp]
theorem bot_ne_top : (⊥ : α) ≠ ⊤ := fun h => not_subsingleton _ <| subsingleton_of_bot_eq_top h

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