instIsEmptySuccOrderOfNonempty — Mathlib

English

If α is nonempty, PredOrder on WithTop α is empty.

Русский

Если α непусто, PredOrder(WithTop α) пуст.

LaTeX

$$$$ \text{IsEmpty}(PredOrder(WithTop(\\alpha))) $$$$

Lean4

instance [hα : Nonempty α] : IsEmpty (SuccOrder (WithBot α)) :=
  ⟨by
    intro
    cases h : succ (⊥ : WithBot α) with
    | bot => exact hα.elim fun a => (max_of_succ_le h.le).not_lt <| bot_lt_coe a
    | coe a =>
      obtain ⟨c, hc⟩ := exists_lt a
      rw [← coe_lt_coe, ← h] at hc
      exact (succ_le_of_lt (bot_lt_coe _)).not_gt hc⟩

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