map_erase — Mathlib

English

For an embedding f, mapping the erase of a under f equals erasing f(a) from the mapped set: map f (s.erase a) = (map f s).erase (f a).

Русский

Для вложения f выполняется равенство: map f (s.erase a) = (map f s).erase (f a).

LaTeX

$$$ (\\,s\\erase a\\,).image f = (\\,s.image f\\,).erase (f a) $$$

Lean4

@[simp]
theorem map_erase [DecidableEq α] (f : α ↪ β) (s : Finset α) (a : α) : (s.erase a).map f = (s.map f).erase (f a) :=
  by
  simp_rw [map_eq_image]
  exact s.image_erase f.2 a

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