map_symmDiff' — Mathlib

English

Boolean-algebra homomorphisms preserve symmetric difference: f(a ∆ b) = f(a) ∆ f(b).

Русский

Гомоморфизм булевой алгебры сохраняет симметрическую разность: f(a ∆ b) = f(a) ∆ f(b).

LaTeX

$$$f(a \Delta b) = f(a) \Delta f(b)$$$

Lean4

/-- Special case of `map_symmDiff` for Boolean algebras. -/
theorem map_symmDiff' (a b : α) : f (a ∆ b) = f a ∆ f b := by rw [symmDiff, symmDiff, map_sup, map_sdiff', map_sdiff']

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