symmDiff_sdiff

Mathlib.Order.SymmDiff

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

English

a Δ b \\ c = (a \\ (b ⊔ c)) ⊔ (b \\ (a ⊔ c)).

Русский

a Δ b \ c = (a \\ (b ⊔ c)) ⊔ (b \\ (a ⊔ c)).

LaTeX

$$$$ a \\Delta b \\\\ c = (a \\\\ (b \\cup c)) \\sqcup (b \\\\ (a \\cup c)) $$$$

Lean4

theorem symmDiff_sdiff : a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) := by
  rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]

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

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

Разделы

Аффилиация

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