succ_eq_bot — Mathlib

English

In a nontrivial linear order, for any a, succ a = ⊥ iff a = ⊥.

Русский

В неабсолютно тривиальном линейном порядке для любого a верно: succ a = ⊥ тогда и только тогда, когда a = ⊥.

LaTeX

$$$$ \forall a:\mathrm{WithBot}\,\alpha,\operatorname{succ} a = \bot \iff a = \bot $$$$

Lean4

@[simp]
theorem succ_eq_bot (a : WithBot α) : WithBot.succ a = ⊥ ↔ a = ⊥ :=
  by
  cases a
  · simp
  · simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false]
    apply ne_of_gt
    by_contra! h
    have h₂ : _ = ⊥ := le_bot_iff.mp ((Order.le_succ _).trans h)
    exact not_isMax_bot (h₂ ▸ Order.max_of_succ_le (h.trans bot_le))

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