symmDiff_eq_sup_sdiff_inf

Mathlib.Order.SymmDiff

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

English

The symmetric difference equals the join of a and b minus their meet: a Δ b = (a ⊔ b) \\ (a ⊓ b).

Русский

Симметрическая разность равна объединению мин и разности: a Δ b = (a ⊔ b) \\ (a ⊓ b).

LaTeX

$$$$ a \\Delta b = (a \\lor b) \\setminus (a \\land b) $$$$

Lean4

theorem symmDiff_eq_sup_sdiff_inf : a ∆ b = (a ⊔ b) \ (a ⊓ b) := by simp [sup_sdiff, symmDiff]

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

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

Разделы

Аффилиация

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