instIsEmptyPredOrderOfNonempty — Mathlib

English

If α is nonempty, then PredOrder(WithTop α) is empty.

Русский

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

LaTeX

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

Lean4

instance [hα : Nonempty α] : IsEmpty (PredOrder (WithTop α)) :=
  ⟨by
    intro
    cases h : pred (⊤ : WithTop α) with
    | top => exact hα.elim fun a => (min_of_le_pred h.ge).not_lt <| coe_lt_top a
    | coe a =>
      obtain ⟨c, hc⟩ := exists_gt a
      rw [← coe_lt_coe, ← h] at hc
      exact (le_pred_of_lt (coe_lt_top c)).not_gt hc⟩

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