noBotOrder — Mathlib

English

Same as the previous density statement with alternate formulation.

Русский

Тот же факт плотности, но другой формализм.

LaTeX

$$$a < b \\iff \\exists x:\\alpha, a < \\mathrm{WithTop}\\,\\preimage x \\land \\mathrm{WithTop}\\,\\preimage x < b$$$

Lean4

instance noBotOrder [LE α] [NoBotOrder α] [Nonempty α] : NoBotOrder (WithTop α) where
  exists_not_ge := fun
    | ⊤ => ‹Nonempty α›.elim fun a ↦ ⟨a, by simp⟩
    | (a : α) =>
      let ⟨b, hba⟩ := exists_not_ge a;
      ⟨b, mod_cast hba⟩

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