disjoint_image_left — Mathlib

English

The image of a set under f is disjoint from t if and only if the original set is disjoint from the preimage of t: Disjoint(f[S], T) ⇔ Disjoint(S, f^{-1}(T)).

Русский

Образ множества S под действием f не пересекается с T тогда и только тогда, когда сам S не пересекается с предобразом T: Disjoint(f[S], T) ⇔ Disjoint(S, f^{-1}(T)).

LaTeX

$$$\\operatorname{Disjoint}(f[S], T) \\iff \\operatorname{Disjoint}(S, f^{-1}(T))$$$

Lean4

theorem disjoint_image_left {f : α → β} {s : Set α} {t : Set β} : Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t) := by
  simp_rw [disjoint_iff_inter_eq_empty, ← not_nonempty_iff_eq_empty, image_inter_nonempty_iff]

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