English
For any function f and sets S ⊆ A, T ⊆ B, the image of the intersection S ∩ f^{-1}(T) under f equals the intersection of the image of S with T: f[S ∩ f^{-1}(T)] = f[S] ∩ T.
Русский
Для любой функции f и множеств S ⊆ A, T ⊆ B выполняется: образ множества S ∩ f^{-1}(T) при отображении f совпадает с пересечением образа S и T: f[S ∩ f^{-1}(T)] = f[S] ∩ T.
LaTeX
$$$f[S \\cap f^{-1}(T)] = f[S] \\cap T$$$
Lean4
theorem image_inter_preimage (f : α → β) (s : Set α) (t : Set β) : f '' (s ∩ f ⁻¹' t) = f '' s ∩ t := by grind