symmDiff_right

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#Disjoint.symmDiff_right

English

If a ⊥ b and a ⊥ c, then a ⊥ b Δ c.

Русский

Если a ⊥ b и a ⊥ c, то a ⊥ (b Δ c).

LaTeX

$$$ Disjoint(a,b) \land Disjoint(a,c) \Rightarrow Disjoint(a \\Delta b, c)$$$

Lean4

protected theorem symmDiff_right (ha : Disjoint a b) (hb : Disjoint a c) : Disjoint a (b ∆ c) :=
  (ha.symm.symmDiff_left hb.symm).symm

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

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

Разделы

Аффилиация

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