diff_eq_filter — Mathlib

English

For a nodup list l, the difference l \\' l2 equals the filter of l by the predicate a ∉ l2.

Русский

Для нодуп-листа l различие l \\\\ l2 равняется фильтру l по условию a ∉ l2.

LaTeX

$$$ \\operatorname{Nodup}(l) \\Rightarrow l \\setminus l_2 = \\operatorname{filter}\\,(\\lambda a. a \\notin l_2)\\ l. $$$

Lean4

theorem diff_eq_filter [BEq α] [LawfulBEq α] : ∀ {l₁ l₂ : List α} (_ : l₁.Nodup), l₁.diff l₂ = l₁.filter (· ∉ l₂)
  | l₁, [], _ => by simp
  | l₁, a :: l₂, hl₁ =>
    by
    rw [diff_cons, (hl₁.erase _).diff_eq_filter, hl₁.erase_eq_filter, filter_filter]
    simp only [decide_not, bne, Bool.and_comm, decide_mem_cons, Bool.not_or]

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