isTotal_le — Mathlib

English

If α is a total order, IsTotal_le holds on WithTop(α): any two elements are comparable.

Русский

Если α упорядочено как общее, то WithTop(α) имеет свойство IsTotal_le: любые два элемента сравнимы.

LaTeX

$$$$ \\text{IsTotal}(\\mathrm{WithTop}(\\alpha)) \\;\\text{ along }\\; \\mathrm{WithTop}(\\le). $$$$

Lean4

instance isTotal_le [LE α] [IsTotal α (· ≤ ·)] : IsTotal (WithTop α) (· ≤ ·) where
  total x y := by cases x <;> cases y <;> simp; simpa using IsTotal.total ..

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