image_sdiff — Mathlib

English

If f is injective, then image under f distributes over set difference: (s \ t).image f = s.image f \ t.image f.

Русский

Если f инъективна, то образ разности распределяется над: (s \ t).image f = s.image f \ t.image f.

LaTeX

$$$\text{Injective } f \Rightarrow (s \backslash t).image f = s.image f \backslash t.image f$$$

Lean4

theorem image_sdiff [DecidableEq α] {f : α → β} (s t : Finset α) (hf : Injective f) :
    (s \ t).image f = s.image f \ t.image f :=
  mod_cast Set.image_diff hf s t

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