English
For an injective map f, the image of the symmetric difference equals the symmetric difference of the images.
Русский
При инъективном отображении f изображение симметрической разности равно симметрической разности изображений.
LaTeX
$$$ (s \\Delta t)^{\\!\\mathrm{image} f} = s^{\\mathrm{image} f} \\Delta t^{\\mathrm{image} f} $$$
Lean4
theorem image_symmDiff [DecidableEq β] {f : α → β} (s t : Finset α) (hf : Injective f) :
(s ∆ t).image f = s.image f ∆ t.image f :=
mod_cast Set.image_symmDiff hf s t