image_inter_nonempty_iff — Mathlib

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]

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