sym_filterNe_mem — Mathlib

English

Membership in the symmetric difference satisfies a ∈ s ∆ t iff a ∈ s and a ∉ t or a ∈ t and a ∉ s.

Русский

Членство в симметрической разности выполняется: a ∈ s ∆ t тогда и только если a ∈ s и a ∉ t или a ∈ t и a ∉ s.

LaTeX

$$$ a \\in s \\Delta t \\iff (a \\in s \\wedge a \\notin t) \\lor (a \\in t \\wedge a \\notin s) $$$

Lean4

theorem sym_filterNe_mem {m : Sym α n} (a : α) (h : m ∈ s.sym n) :
    (m.filterNe a).2 ∈ (Finset.erase s a).sym (n - (m.filterNe a).1) :=
  mem_sym_iff.2 fun b H ↦ mem_erase.2 <| (Multiset.mem_filter.1 H).symm.imp Ne.symm <| mem_sym_iff.1 h b

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