English
Let ι be an index set, α(i) a family of sets, and v(i) subsets of α(i). If the product ∏ i α(i) with coordinates in v(i) is nonempty, then the i-th projection of the intersection of the corresponding preimages equals v(i).
Русский
Пусть ι — множество индексов, α(i) — семейство множеств, v(i) ⊆ α(i). Если произведение ∏ i α(i) с координатами в v(i) непусто, то i-ая проекция пересечения соответствующих прообразов равна v(i).
LaTeX
$$$( (\\text{image}\\, (x \\mapsto x_i)) \\, (\\bigcap_k (\\text{preimage}\\, (x \\mapsto x_k)\\, (v_k))) ) = v_i$$$
Lean4
theorem kernImage_preimage_union {s : Set α} {t : Set β} : kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s := by
rw [union_comm, kernImage_union_preimage, union_comm]
