pred_eq_top — Mathlib

English

For Nontrivial α with LinearOrder, pred a = ⊤ iff a = ⊤.

Русский

Для ненулевого α с линейным порядком pred a = ⊤ тогда и только тогда, когда a = ⊤.

LaTeX

$$$$ \forall a:\mathrm{WithTop}\,\alpha,\operatorname{pred} a = \top \iff a = \top $$$$

Lean4

@[simp]
theorem pred_eq_top (a : WithTop α) : WithTop.pred a = ⊤ ↔ a = ⊤ :=
  by
  cases a
  · simp
  · simp only [WithTop.pred_coe, WithTop.coe_ne_top, iff_false]
    apply ne_of_lt
    by_contra! h
    have h₂ : _ = ⊤ := top_le_iff.mp (h.trans (Order.pred_le _))
    exact not_isMin_top (h₂ ▸ Order.min_of_le_pred (le_top.trans h))

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