coe_symmDiff — Mathlib

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]

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