English
If f is injective, then (s.erase a).image f = (s.image f).erase (f a).
Русский
Если f инъективна, то образ удаления элемента равен образу множества после удаления образа элемента: (s.erase a).image f = (s.image f).erase (f a).
LaTeX
$$$\text{Injective } f \Rightarrow (s.erase a).image f = (s.image f).erase (f a)$$$
Lean4
@[simp]
theorem image_erase [DecidableEq α] {f : α → β} (hf : Injective f) (s : Finset α) (a : α) :
(s.erase a).image f = (s.image f).erase (f a) :=
coe_injective <| by push_cast [Set.image_diff hf, Set.image_singleton]; rfl