eq_bot_of_minimal — Mathlib

English

If an element a has no smaller element than it, then a must be the bottom element: if ∀ b, not b < a, then a = ⊥.

Русский

Если элемент a минимален по отношению к ≤, то он равен нижнему элементу: если для всех b выполняется ¬(b < a), то a = ⊥.

LaTeX

$$$\forall b, \neg b < a \quad\Rightarrow\quad a = \bot$$$

Lean4

theorem eq_bot_of_minimal (h : ∀ b, ¬b < a) : a = ⊥ :=
  (eq_bot_or_bot_lt a).resolve_right (h ⊥)

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