antisymmRel_swap — Mathlib

English

Swapping the underlying relation does not change the antisymmetric relation: AntisymmRel(swap r) = AntisymmRel r.

Русский

Замена порядка на его двойственный не меняет антисимметричность: AntisymmRel(swap r) = AntisymmRel r.

LaTeX

$$$\operatorname{AntisymmRel}(\text{swap } r) = \operatorname{AntisymmRel}(r)$$$

Lean4

theorem antisymmRel_swap : AntisymmRel (swap r) = AntisymmRel r :=
  funext₂ fun _ _ ↦ propext and_comm

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