disjoint_preimage_iff — Mathlib

English

For surjective f, Disjoint f^{-1}(s) and f^{-1}(t) iff Disjoint s and t.

Русский

Для сюръективной f, непересечение прообразов f^{-1}(s) и f^{-1}(t) эквивалентно непересечности s и t.

LaTeX

$$$\operatorname{Disjoint}(f^{-1}(s), f^{-1}(t)) \iff \operatorname{Disjoint}(s,t)$$$

Lean4

@[simp]
theorem disjoint_preimage_iff (hf : Surjective f) {s t : Set β} : Disjoint (f ⁻¹' s) (f ⁻¹' t) ↔ Disjoint s t :=
  ⟨Disjoint.of_preimage hf, Disjoint.preimage _⟩

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