bihimp_right

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#Codisjoint.bihimp_right

English

If a is codisjoint from b and from c, then a is codisjoint from (b ⇔ c).

Русский

Если a кодиссоиден с b и с c, то a кодиссоиден с (b ⇔ c).

LaTeX

$$$ (ha: Codisjoint\, a\, b) (hb: Codisjoint\, a\, c) \Rightarrow Codisjoint\, a\, (b \Leftrightarrow c) $$$

Lean4

protected theorem bihimp_right (ha : Codisjoint a b) (hb : Codisjoint a c) : Codisjoint a (b ⇔ c) :=
  (ha.inf_right hb).mono_right inf_le_bihimp

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

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

Разделы

Аффилиация

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