rel_id — Mathlib

English

For any index i, the generating relation evaluated at i matches the identity relation on the element lof and 1.

Русский

Для любого индекса i применение генераторной связи к i даёт тождество на элементе lof и единице.

LaTeX

$$$\\text{rel\_id }(i) :\\; \\text{rel } R A \\; (ι R (\\text{lof } R I A i\, 1))\, 1 = \\text{rel.id}$$$

Lean4

theorem rel_id (i : I) : rel R A (ι R <| lof R I A i 1) 1 :=
  rel.id

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