preimage_eq_empty_iff — Mathlib

English

For any f, f^{-1}(s) = ∅ iff Disjoint s and range f.

Русский

Для любого отображения f, f^{-1}(s) = ∅ тогда и только тогда, когда s несовпадает с диапазоном f.

LaTeX

$$$ f^{-1}(s) = \emptyset \iff \operatorname{Disjoint}(s, \operatorname{range}(f)) $$$

Lean4

theorem preimage_eq_empty_iff {s : Set β} : f ⁻¹' s = ∅ ↔ Disjoint s (range f) :=
  ⟨fun h => by
    simp only [eq_empty_iff_forall_notMem, disjoint_iff_inter_eq_empty, mem_preimage] at h ⊢
    grind, preimage_eq_empty⟩

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