noMinOrder — Mathlib

English

If α has LT, NoMinOrder, and is Nonempty, then WithTop α has NoMinOrder.

Русский

Если α имеет LT, NoMinOrder и непустое, то WithTop α имеет NoMinOrder.

LaTeX

$$$\\operatorname{NoMinOrder}(\\mathrm{WithTop}\\,\\alpha)$ given LT α, NoMinOrder α, Nonempty α.$$

Lean4

instance noMinOrder [LT α] [NoMinOrder α] [Nonempty α] : NoMinOrder (WithTop α) where
  exists_lt := fun
    | ⊤ => ‹Nonempty α›.elim fun a ↦ ⟨a, by simp⟩
    | (a : α) =>
      let ⟨b, hab⟩ := exists_lt a;
      ⟨b, mod_cast hab⟩

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