swap — Mathlib

English

If a relation R on a set A is asymmetric, then the swapped relation on A is asymmetric as well.

Русский

Если отношение R на множестве A асимметрично, то переставленное отношение тоже асимметрично.

LaTeX

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

Lean4

theorem swap (r) [IsAsymm α r] : IsAsymm α (swap r) :=
  ⟨fun _ _ h₁ h₂ => asymm_of r h₂ h₁⟩

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