not_top_lt — Mathlib

English

Let α be a type with a strict order. For every x in WithTop(α), the top element is not strictly less than x.

Русский

Пусть α — множество с строгим порядком. Для любого x ∈ WithTop(α) верно: ⊤ не меньше x в строгом сравнении.

LaTeX

$$$$ \\forall x: \\mathrm{WithTop}(\\alpha), \\neg (\\top < x). $$$$

Lean4

@[simp]
protected theorem not_top_lt (a : WithTop α) : ¬⊤ < a := by simp [lt_def]

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