rel_congr_right

Mathlib.Order.Defs.Unbundled

URI: https://scilib.ai/kg/mathlib#rel_congr_right

English

Right congruence: given r b c, then r a b ↔ r a c for any a.

Русский

Право-конгруэнтность: при r b c имеем r a b ⇔ r a c для любого a.

LaTeX

$$$\\\\forall a,b,c, \\\\ r(b,c) \\\\Rightarrow \\\\ r(a,b) \\\\Leftrightarrow \\\\ r(a,c).$$$

Lean4

theorem rel_congr_right [IsSymm α r] [IsTrans α r] {a b c : α} (h : r b c) : r a b ↔ r a c :=
  ⟨(trans_of r · h), (trans_of r · (symm_of r h))⟩

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

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

Разделы

Аффилиация

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