isTotal — Mathlib

English

If β is a total order, then β* is a total order under ≤.

Русский

Если β является полным порядком, то β* также является полным порядком относительно ≤.

LaTeX

$$$\\text{IsTotal}(β, \\le) \\Rightarrow \\text{IsTotal}(β^*, \\le).$$$

Lean4

instance isTotal [LE β] [IsTotal β (· ≤ ·)] : IsTotal β* (· ≤ ·) :=
  ⟨fun f g => inductionOn₂ f g fun _f _g => eventually_or.1 <| Eventually.of_forall fun _x => total_of _ _ _⟩

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