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 subset_image_symmDiff : (f '' s) ∆ (f '' t) ⊆ f '' s ∆ t :=
(union_subset_union (subset_image_diff _ _ _) <| subset_image_diff _ _ _).trans (superset_of_eq (image_union _ _ _))