sumPiEquivProdPi_symm_preimage_univ_pi

English

Duplicate of sumPiEquivProdPi_symm_preimage_univ_pi, same decomposition.

Русский

Дубликат: то же разложение предобраза через сумму/произведение.

LaTeX

$$$$ (\\text{sumPiEquivProdPi } \\pi)^{-1}' \\mathrm{univ}.\\pi t = \\mathrm{univ}.\\pi (\\lambda i. t(\\mathrm{inl}\, i)) \\times \\mathrm{univ}.\\pi (\\lambda i. t(\\mathrm{inr}\, i)). $$$$

Lean4

theorem sumPiEquivProdPi_symm_preimage_univ_pi (π : ι ⊕ ι' → Type*) (t : ∀ i, Set (π i)) :
    (sumPiEquivProdPi π).symm ⁻¹' univ.pi t = univ.pi (fun i => t (.inl i)) ×ˢ univ.pi fun i => t (.inr i) :=
  by
  ext
  simp

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