realize_antisymmetric — Mathlib

English

Antisymmetry of r is reflected by Realize of the corresponding sentence on RelMap.

Русский

Антисимметричность r отражается через Realize соответствующего предложения на RelMap.

LaTeX

$$$M \vDash r.antisymmetric \iff AntiSymmetric (\lambda x y. \mathrm{RelMap } r ![x,y])$$$

Lean4

@[simp]
theorem realize_antisymmetric : M ⊨ r.antisymmetric ↔ AntiSymmetric fun x y : M => RelMap r ![x, y] :=
  forall_congr' fun _ => forall_congr' fun _ => imp_congr realize_rel₂ (imp_congr realize_rel₂ Iff.rfl)

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