toFinset_symmDiff — Mathlib

English

If (s ∆ t) is finite, then its Finset equals the symmetric difference of the Finsets: h.toFinset = hs.toFinset ∆ ht.toFinset.

Русский

Если (s ∆ t) конечно, то соответствующий Finset равен симметрической разности Finset: h.toFinset = hs.toFinset ∆ ht.toFinset.

LaTeX

$$$ h.toFinset = hs.toFinset \triangle ht.toFinset $$$

Lean4

protected theorem toFinset_symmDiff [DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∆ t).Finite) :
    h.toFinset = hs.toFinset ∆ ht.toFinset := by
  ext
  simp [mem_symmDiff, Finset.mem_symmDiff]

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