English
A restatement of the previous result: for appropriate sets, the i-th projection of the intersection of projected preimages equals v_i.
Русский
Переформулировка предыдущего результата: для соответствующих множеств i-я проекция пересечения прообразов равна v_i.
LaTeX
$$$((\\text{image}\\, (\\lambda x: x_i))(\\bigcap_k (\\text{preimage}\\, (\\lambda x: x_k)\\,(v_k)))) = v_i$$$
Lean4
theorem image_projection_prod {ι : Type*} {α : ι → Type*} {v : ∀ i : ι, Set (α i)} (hv : (pi univ v).Nonempty) (i : ι) :
((fun x : ∀ i : ι, α i => x i) '' ⋂ k, (fun x : ∀ j : ι, α j => x k) ⁻¹' v k) = v i := by
classical
apply Subset.antisymm
· simp [iInter_subset]
· intro y y_in
simp only [mem_image, mem_iInter, mem_preimage]
rcases hv with ⟨z, hz⟩
refine ⟨Function.update z i y, ?_, update_self i y z⟩
rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
exact ⟨y_in, fun j _ => by simpa using hz j⟩
