subset_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 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 _ _ _))

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