exact

Mathlib.Data.Sym.Sym2

URI: https://scilib.ai/kg/mathlib#Sym2.exact

English

If Sym2.mk p = Sym2.mk p' then p Rel p'.

Русский

Если Sym2.mk p = Sym2.mk p', тогда p Rel p'.

LaTeX

$$$$ Sym2.mk(p) = Sym2.mk(p') \Rightarrow Sym2.Rel\alpha\ p\ p'. $$$$

Lean4

protected theorem exact {p p' : α × α} (h : Sym2.mk p = Sym2.mk p') : Sym2.Rel α p p' :=
  Quotient.exact (s := Sym2.Rel.setoid α) h

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

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

Разделы

Аффилиация

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