eqv — Mathlib

English

The relation 'is a rotation of' is an equivalence relation on lists: reflexive, symmetric, and transitive.

Русский

Отношение «является вращением» является отношением эквивалентности на списках: рефлексивность, симметричность и транзитивность.

LaTeX

$$$ \sim_{\mathrm{rot}} \text{ on List}(\alpha) \text{ is an equivalence relation}$$$

Lean4

theorem eqv : Equivalence (@IsRotated α) :=
  Equivalence.mk IsRotated.refl IsRotated.symm IsRotated.trans

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