swap — Mathlib

English

If a relation R on a set A is total, then the swapped relation on A is total.

Русский

Если отношение R на множестве A полностью упорядочено (тотально), то переставленное отношение тоже полностью упорядочено.

LaTeX

$$$\\forall \\alpha\\;\\forall r:\\alpha \\to \\alpha \\to \\mathrm{Prop},\\; \\Big(\\forall a,b:\\alpha,\\; r\\,a\\,b \\lor r\\,b\\,a\\Big) \\rightarrow \\Big(\\forall a,b:\\alpha,\\; r\\,b\\,a \\lor r\\,a\\,b\\Big)$$$

Lean4

theorem swap (r) [IsTotal α r] : IsTotal α (swap r) :=
  ⟨fun a b => (total_of r a b).symm⟩

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