eq

Mathlib.Logic.Pairwise

URI: https://scilib.ai/kg/mathlib#Pairwise.eq

English

If r is pairwise, then not r a b implies a = b.

Русский

Если r держится попарно, то неравенство r a b приводит к равенству a = b.

LaTeX

$$$\\operatorname{Pairwise}(r) \\rightarrow \\lnot r(a,b) \\Rightarrow a=b$$$

Lean4

protected theorem eq (h : Pairwise r) : ¬r a b → a = b :=
  not_imp_comm.1 <| @h _ _

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

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

Разделы

Аффилиация

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