rel_congr_left

Mathlib.Order.Defs.Unbundled

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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