inf_sup_symmDiff

Mathlib.Order.SymmDiff

URI: https://scilib.ai/kg/mathlib#inf_sup_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_sup_symmDiff : a ⊓ b ⊔ a ∆ b = a ⊔ b := by rw [sup_comm, symmDiff_sup_inf]

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

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

Разделы

Аффилиация

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