map_symmDiff — Mathlib

English

Let f be a homomorphism between co-Heyting algebras. Then f preserves symmetric difference: for all a,b in α, f(a ∆ b) = f(a) ∆ f(b).

Русский

Пусть f — гомоморфизм когейтинговых алгебр. Тогда f сохраняет симметрическую разность: для любых a,b ∈ α выполняется f(a ∆ b) = f(a) ∆ f(b).

LaTeX

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

Lean4

@[simp]
theorem map_symmDiff (a b : α) : f (a ∆ b) = f a ∆ f b := by simp_rw [symmDiff, map_sup, map_sdiff]

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