isTotal_le — Mathlib

English

If α is a total order, then WithZero α is a total order; any two elements are comparable by ≤.

Русский

Если α — это полный порядок, то WithZero α тоже имеет полный порядок; любые два элемента сопоставимы по отношению ≤.

LaTeX

$$$\operatorname{Preorder}(\alpha) \land \operatorname{IsTotal}(\alpha, \le) \Rightarrow \operatorname{IsTotal}(\mathrm{WithZero}\,\alpha, \le)$$$

Lean4

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

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