of_preimage — Mathlib

English

If f is surjective and the preimages f^{-1}(s) and f^{-1}(t) are disjoint, then s and t are disjoint.

Русский

Если f-surjective и f^{-1}(s) и f^{-1}(t) непересекаются, то s и t непересекаются.

LaTeX

$$$\operatorname{Disjoint}(s,t) \Leftarrow \operatorname{Disjoint}(f^{-1}(s), f^{-1}(t))$ (при сюръективности f)$$

Lean4

theorem _root_.Disjoint.of_preimage (hf : Surjective f) {s t : Set β} (h : Disjoint (f ⁻¹' s) (f ⁻¹' t)) :
    Disjoint s t := by
  rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq, image_empty]

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