sound

Mathlib.Data.Sym.Sym2

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

English

If p is related to p' under Rel α, then Sym2.mk p = Sym2.mk p'.

Русский

Если p Rel α p', то классы эквивалентности [p] и [p'] совпадают: Sym2.mk p = Sym2.mk p'.

LaTeX

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

Lean4

protected theorem sound {p p' : α × α} (h : Sym2.Rel α p p') : Sym2.mk p = Sym2.mk p' :=
  Quot.sound h

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

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

Разделы

Аффилиация

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