image_symmDiff — Mathlib

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

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