symmDiff_left

Mathlib.Order.SymmDiff

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

protected theorem symmDiff_left (ha : Disjoint a c) (hb : Disjoint b c) : Disjoint (a ∆ b) c :=
  by
  rw [symmDiff_eq_sup_sdiff_inf]
  exact (ha.sup_left hb).disjoint_sdiff_left

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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