inf_symmDiff_symmDiff

Mathlib.Order.SymmDiff

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

English

(A ∩ B) Δ (A Δ B) = A ∪ B.

Русский

(A ∩ B) Δ (A Δ B) = A ∪ B.

LaTeX

$$$$ (A \\cap B) \\Delta (A \\Delta B) = A \\cup B $$$$

Lean4

@[simp]
theorem inf_symmDiff_symmDiff : (a ⊓ b) ∆ (a ∆ b) = a ⊔ b := by rw [symmDiff_comm, symmDiff_symmDiff_inf]

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

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

Разделы

Аффилиация

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