English
Mapping an injective function f preserves disjointness of the symmetric difference of two lists: map f (l1.diff l2) = (map f l1).diff (map f l2).
Русский
Образ под инъективной функцией f сохраняет непересечение разности двух списков: map f (l1.diff l2) = (map f l1).diff (map f l2).
LaTeX
$$$ \\text{map}_f(l_1.\\text{diff } l_2) = (\\text{map}_f l_1).\\text{diff}(\\text{map}_f l_2) $$$
Lean4
@[simp]
theorem map_diff [DecidableEq β] {f : α → β} (finj : Injective f) {l₁ l₂ : List α} :
map f (l₁.diff l₂) = (map f l₁).diff (map f l₂) := by simp only [diff_eq_foldl, foldl_map, map_foldl_erase finj]
