is_equivalence

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.EqvGen.is_equivalence

English

For any relation r, the generated equivalence EqvGen r is an equivalence relation.

Русский

Для любого отношения r множество EqvGen r образует эквивалентность.

LaTeX

$$$\\\\operatorname{Equivalence}(\\\\operatorname{EqvGen} r)$$$

Lean4

theorem is_equivalence : Equivalence (@EqvGen α r) :=
  Equivalence.mk EqvGen.refl (EqvGen.symm _ _) (EqvGen.trans _ _ _)

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

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

Разделы

Аффилиация

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