isTotal_le — Mathlib

English

If α is a partially ordered set with a least upper bound property and is totally ordered, then WithBot α is totally ordered under ≤.

Русский

Если α упорядочено так, что любое два элемента сравнимы (полный порядок), тогда WithBot α также является полностью упорядоченным относительно ≤.

LaTeX

$$$IsTotal(WithBot, \le) \Leftarrow IsTotal(α, \le)$$$

Lean4

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

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