kernImage_union_preimage — Mathlib

English

For sets s and t, the kernImage of the union with the preimage of t equals the union of kernImage f s and t: kernImage f (s ∪ f^{-1}(t)) = kernImage f s ∪ t.

Русский

Для множеств s и t верно: kernImage f (s ∪ f^{-1}(t)) = kernImage f s ∪ t.

LaTeX

$$$\\mathrm{kernImage}\\, f\\, (s \\cup f^{-1}(t)) = \\mathrm{kernImage}\\, f\\, s \\cup t$$$

Lean4

theorem kernImage_union_preimage {s : Set α} {t : Set β} : kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t := by
  rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage, compl_inter,
    compl_compl]

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