kernImage_preimage_eq_iff — Mathlib

English

For a set s ⊆ β, kernImage f (f^{-1}(s)) = s if and only if (range f)^c ⊆ s.

Русский

Для s ⊆ β верно: kernImage f (f^{-1}(s)) = s тогда и только тогда, когда (range f)^c ⊆ s.

LaTeX

$$$\\mathrm{kernImage}\\, f\\, (f^{-1}(s)) = s \\iff (\\mathrm{range}\\, f)^c \\subseteq s$$$

Lean4

theorem kernImage_preimage_eq_iff {s : Set β} : kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s := by
  rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff, compl_subset_comm]

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