lt_succ_bot_iff — Mathlib

English

In a linear order with a bottom element ⊥ and a successor operation, if there is no maximum, then a < succ(⊥) holds only for a = ⊥.

Русский

В линейном порядке с нижним элементом ⊥ и операцией следующего, при отсутствии максимума выполняется: a < succ(⊥) тогда и только тогда, когда a = ⊥.

LaTeX

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

Lean4

theorem lt_succ_bot_iff [NoMaxOrder α] : a < succ ⊥ ↔ a = ⊥ := by rw [lt_succ_iff, le_bot_iff]

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