English
The intersection of the image f[S] with T is nonempty if and only if the intersection S ∩ f^{-1}(T) is nonempty: (f[S] ∩ T) ≠ ∅ ⇔ (S ∩ f^{-1}(T)) ≠ ∅.
Русский
Пересечение образа f[S] с T непусто тогда и только тогда, когда пересечение S и f^{-1}(T) непусто: (f[S] ∩ T) ≠ ∅ ⇔ (S ∩ f^{-1}(T)) ≠ ∅.
LaTeX
$$$(f[S] \\cap T) \\neq \\emptyset \\iff (S \\cap f^{-1}(T)) \\neq \\emptyset$$$
Lean4
@[simp]
theorem image_inter_nonempty_iff {f : α → β} {s : Set α} {t : Set β} : (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty :=
by rw [← image_inter_preimage, image_nonempty]