image_symmDiff — Mathlib

English

If f is injective, then the image of the symmetric difference equals the symmetric difference of the images: f[S ∆ T] = f[S] ∆ f[T].

Русский

Если f инъективна, то образ симметрической разности равен симметрической разности образов: f[S ∆ T] = f[S] ∆ f[T].

LaTeX

$$$$ f[S \triangle T] = f[S] \triangle f[T]. $$$$

Lean4

theorem image_symmDiff (hf : Injective f) (s t : Set α) : f '' s ∆ t = (f '' s) ∆ (f '' t) := by
  simp_rw [Set.symmDiff_def, image_union, image_diff hf]

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