le_succ_bot_iff — Mathlib

English

Let α be a linear order with a bottom element and a successor operation. For any a, a is ≤ succ(⊥) if and only if a = ⊥ or a = succ(⊥).

Русский

Пусть α — линейный порядок с нижним элементом и операцией successor. Для любого a выполняется: a ≤ succ(⊥) тогда и только тогда, когда a = ⊥ или a = succ(⊥).

LaTeX

$$$ a \le \operatorname{succ}(\bot) \iff a = \bot \ \lor\ a = \operatorname{succ}(\bot) $$$

Lean4

theorem le_succ_bot_iff : a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥ := by rw [le_succ_iff_eq_or_le, le_bot_iff, or_comm]

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