lt_top — Mathlib

English

Let α be a partially ordered set with a top element ⊤. If a is not equal to ⊤, then a is strictly below ⊤, i.e., a < ⊤.

Русский

Пусть α — частично упорядоченное множество с верхним элементом ⊤. Если a ≠ ⊤, то a строго меньше ⊤, то есть a < ⊤.

LaTeX

$$$\forall a:\\alpha,\ a \neq \top \\rightarrow a < \top$$$

Lean4

@[aesop (rule_sets := [finiteness]) safe apply]
theorem lt_top (h : a ≠ ⊤) : a < ⊤ :=
  lt_top_iff_ne_top.mpr h

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