image_compl_preimage — Mathlib

English

For any f and s, the image of the complement of the preimage of s equals the range of f minus s.

Русский

Для любой функции f и подмножества s выполняется равенство: образ комплемента предобраза s равен range(f) \ s.

LaTeX

$$$$ f''(f^{-1}(s))^{c} = \\operatorname{range}(f) \\setminus s $$$$

Lean4

theorem image_compl_preimage {f : α → β} {s : Set β} : f '' (f ⁻¹' s)ᶜ = range f \ s := by
  rw [compl_eq_univ_diff, image_diff_preimage, image_univ]

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