bot_ne_top — Mathlib

English

In a simple order, the bottom and top are distinct: ⊥ ≠ ⊤.

Русский

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

LaTeX

$$$(\bot : α) \neq (\top : α)$$$

Lean4

theorem bot_ne_top [LE α] [BoundedOrder α] [IsSimpleOrder α] : (⊥ : α) ≠ (⊤ : α) :=
  by
  obtain ⟨a, b, h⟩ := exists_pair_ne α
  rcases eq_bot_or_eq_top a with (rfl | rfl) <;> rcases eq_bot_or_eq_top b with (rfl | rfl) <;>
    first
    | simpa
    | simpa using h.symm

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