total — Mathlib

English

If s is a chain under a reflexive relation r, then for any x,y in s, either x precedes y or y precedes x under r.

Русский

Если s — цепь относительно рефлексивного отношения r, то для любых x,y ∈ s либо x предшествует y, либо y предшествует x по r.

LaTeX

$$$ IsChain\\ r\\ s \\rightarrow \\forall x \\in s, \\forall y \\in s, x \\prec y \\lor y \\prec x $$$

Lean4

theorem total (h : IsChain r s) (hx : x ∈ s) (hy : y ∈ s) : x ≺ y ∨ y ≺ x :=
  (eq_or_ne x y).elim (fun e => Or.inl <| e ▸ refl _) (h hx hy)

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