English
If f is injective on u and s ⊆ u and t ⊆ u, then f''(s ∩ t) = f''s ∩ f''t.
Русский
Если f инъективна на u и s ⊆ u, t ⊆ u, то образ пересечения равен пересечению образов.
LaTeX
$$$ \\operatorname{InjOn} f u \\land s \\subseteq u \\land t \\subseteq u \\Rightarrow f '' (s \\cap t) = f '' s \\cap f '' t$$$
Lean4
theorem image_inter {s t u : Set α} (hf : u.InjOn f) (hs : s ⊆ u) (ht : t ⊆ u) : f '' (s ∩ t) = f '' s ∩ f '' t :=
by
apply Subset.antisymm (image_inter_subset _ _ _)
intro x ⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩
have : y = z := by
apply hf (hs ys) (ht zt)
rwa [← hz] at hy
rw [← this] at zt
exact ⟨y, ⟨ys, zt⟩, hy⟩