image_erase — Mathlib

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

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