English
The symmetric difference commutes with coercion to sets: the set-theoretic symmetric difference of s and t equals the coercion of the Finset symmetric difference.
Русский
Симметрическая разность гармонизирует с приведением к множествам: симметрическая разность множества s и t равна каноническому переносу через множества.
LaTeX
$$$ (s \\Delta t)^{\\toSet} = s^{\\toSet} \\Delta t^{\\toSet} $$$
Lean4
@[simp, norm_cast]
theorem coe_symmDiff : (↑(s ∆ t) : Set α) = (s : Set α) ∆ t :=
Set.ext fun x => by simp [mem_symmDiff, Set.mem_symmDiff]