English
If f is injective on s, then f''(s \\ t) = f''s \\ f''(s ∩ t).
Русский
Если f инъективна на s, то образ разности s \\ t равен образу s минус образ s ∩ t: f''(s \\ t) = f''s \\ f''(s ∩ t).
LaTeX
$$$\\forall t\\subseteq α\\, (h:\\, s\\ InjOn\\ f) \\Rightarrow f''(s\\setminus t) = f''s \\setminus f''(s\\cap t).$$$
Lean4
theorem image_diff {t : Set α} (h : s.InjOn f) : f '' (s \ t) = f '' s \ f '' (s ∩ t) :=
by
refine
subset_antisymm (subset_diff.2 ⟨image_mono diff_subset, ?_⟩)
(diff_subset_iff.2 (by rw [← image_union, inter_union_diff]))
exact Disjoint.image disjoint_sdiff_inter h diff_subset inter_subset_left