realize_reflexive — Mathlib

English

For a relation symbol r, realization of its reflexive/antisymmetric properties is equivalent to the corresponding RelMap invariants.

Русский

Для символьного отношения r реализуемость его рефлексивности/антисимметричности эквивалентна соответствующим инвариантам RelMap.

LaTeX

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

Lean4

@[simp]
theorem realize_reflexive : M ⊨ r.reflexive ↔ Reflexive fun x y : M => RelMap r ![x, y] :=
  forall_congr' fun _ => realize_rel₂

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