reorderRestrictProd_mem_preimage_image_restrict

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⟩

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