is_equivalence

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.Rel.is_equivalence

English

The relation Rel α on α×α is an equivalence relation (reflexive, symmetric, and transitive).

Русский

Относитель Rel α на α×α является эквивалентностью: рефлексивен, симметричен и транзитивен.

LaTeX

$$$$ \operatorname{Equivalence}(Rel\,\alpha). $$$$

Lean4

theorem is_equivalence : Equivalence (Rel α) :=
  { refl := fun (x, y) ↦ Rel.refl x y, symm := Rel.symm, trans := Rel.trans }

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru