left_unique

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#IsCompl.left_unique

English

If x is complemented with z and y is complemented with z, then x = y.

Русский

Если x комплементарно связано с z, а y с z, тогда x = y.

LaTeX

$$$$ IsCompl(x,z) \rightarrow IsCompl(y,z) \rightarrow x = y. $$$$

Lean4

theorem left_unique (hxz : IsCompl x z) (hyz : IsCompl y z) : x = y :=
  hxz.symm.right_unique hyz.symm

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

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

Разделы

Аффилиация

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