zigzag_equivalence — Mathlib

English

Zigzag is an equivalence relation on the objects of J.

Русский

Zigzag является эквивалентным отношением на объектах J (по сути: рефлексивность, симметрия, транзитивность).

LaTeX

$$$\text{Equivalence}(\text{Zigzag})$$$

Lean4

theorem zigzag_equivalence : _root_.Equivalence (@Zigzag J _) :=
  _root_.Equivalence.mk Relation.reflexive_reflTransGen (fun h => zigzag_symmetric h)
    (fun h g => Relation.transitive_reflTransGen h g)

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