congr_right

Mathlib.Data.Sym.Sym2

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

English

For a,b,c ∈ α, s(a,b) = s(a,c) if and only if b=c.

Русский

Для произвольных a,b,c ∈ α, s(a,b) = s(a,c) тогда и только тогда, когда b=c.

LaTeX

$$$$ {a,b,c : \alpha} \; s(a,b) = s(a,c) \iff b = c. $$$$

Lean4

theorem congr_right {a b c : α} : s(a, b) = s(a, c) ↔ b = c := by simp +contextual

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

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

Разделы

Аффилиация

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