isTotal — Mathlib

English

The order relation on PartENat is total: for any x,y, either x ≤ y or y ≤ x.

Русский

Порядок на PartENat является тотальным: для любых x,y либо x ≤ y, либо y ≤ x.

LaTeX

$$$ \forall x,y : \mathrm{PartENat}, x \le y \lor y \le x $$$

Lean4

instance isTotal : IsTotal PartENat (· ≤ ·) where
  total x
    y :=
    PartENat.casesOn (P := fun z => z ≤ y ∨ y ≤ z) x (Or.inr le_top)
      (PartENat.casesOn y (fun _ => Or.inl le_top) fun x y =>
        (le_total x y).elim (Or.inr ∘ coe_le_coe.2) (Or.inl ∘ coe_le_coe.2))

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