realize_transitive — Mathlib

English

Transitivity of r is realized by the corresponding RelMap in the sentence Realize.

Русский

Транзитивность r реализуется через RelMap в предложении Realize.

LaTeX

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

Lean4

@[simp]
theorem realize_transitive : M ⊨ r.transitive ↔ Transitive fun x y : M => RelMap r ![x, y] :=
  forall_congr' fun _ =>
    forall_congr' fun _ => forall_congr' fun _ => imp_congr realize_rel₂ (imp_congr realize_rel₂ realize_rel₂)

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