sdiff_symmDiff — Mathlib

English

The symmetric difference of c and a with respect to the set difference equals a certain join of intersections: c \\ a Δ b = c ∧ a ∧ b ∨ c \\ a ∧ c \\ b.

Русский

Симметрическая разность c \\ a Δ b равна объединению: c ∧ a ∧ b ∨ c \\ a ∧ c \\ b.

LaTeX

$$∀ a b c, (c \\ a) \\Delta b = (c ∧ a ∧ b) ∨ (c \\ a ∧ c \\ b)$$

Lean4

theorem sdiff_symmDiff : c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b := by simp only [(· ∆ ·), sdiff_sdiff_sup_sdiff']

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