sdiff_symmDiff_eq_sup

Mathlib.Order.SymmDiff

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem sdiff_symmDiff_eq_sup : (a \ b) ∆ b = a ⊔ b := by rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]

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

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

Разделы

Аффилиация

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