English
Let S be a subset of indices and s a family of functions. For any p in the product of the restricted complement and the restriction to S, applying the reordering map produces an element whose restriction lies in the restricted image of s.
Русский
Пусть S ⊆ ι и s ⊆ ∏ i α_i. Для любого p ∈ (S^c.restrict '' s) × (∏ i∈S α_i) верно, что reorderRestrictProd S s p лежит в (S^c.restrict)^{-1}(S^c.restrict '' s).
LaTeX
$$$\\forall p \\in (S^{c}.\\restrict '' s) \\times (\\prod_{i \\in S} \\alpha_i):\\ reorderRestrictProd\\,S\\,s\\,p \\in (S^{c}.\\restrict)^{-1}\\bigl(S^{c}.\\restrict '' s\\bigr).$$$
Lean4
theorem reorderRestrictProd_mem_preimage_image_restrict (p : Sᶜ.restrict '' s × (Π i : S, α i)) :
reorderRestrictProd S s p ∈ Sᶜ.restrict ⁻¹' (Sᶜ.restrict '' s) :=
by
obtain ⟨y, hy_mem_s, hy_eq⟩ := p.1.2
exact ⟨y, hy_mem_s, hy_eq.trans (restrict_compl_reorderRestrictProd p).symm⟩