English
If a relation R on a set A is antisymmetric, then the opposite (swapped) relation on A is antisymmetric as well.
Русский
Если отношение R на множестве A антисимметрично, то противоположное (переставленное) отношение на A также антисимметрично.
LaTeX
$$$\\forall \\alpha\\;\\forall r:\\alpha \\to \\alpha \\to \\mathrm{Prop},\\; \\Big(\\forall a,b:\\alpha,\\; r\\,a\\,b \\land r\\,b\\,a \\rightarrow a=b\\Big) \\rightarrow \\Big(\\forall a,b:\\alpha,\\; r\\,b\\,a \\land r\\,a\\,b \\rightarrow a=b\\Big)$$$
Lean4
theorem swap (r) [IsAntisymm α r] : IsAntisymm α (swap r) :=
⟨fun _ _ h₁ h₂ => _root_.antisymm h₂ h₁⟩
