top_ne_zero — Mathlib

English

In a linear ordered additive group with top, the top element is not equal to zero.

Русский

В линейно упорядоченной аддитивной группе с верхней границей верхний элемент не равен нулю.

LaTeX

$$$\top \neq 0$$$

Lean4

@[simp]
theorem top_ne_zero : (⊤ : α) ≠ 0 := by
  intro nh
  have ⟨a, b, h⟩ := Nontrivial.exists_pair_ne (α := α)
  have : a + 0 ≠ b + 0 := by simpa
  rw [← nh] at this
  simp at this

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