piCongrLeft_preimage_univ_pi — Mathlib

English

A sum-type to product-type equivalence decomposes preimages into pairwise products over left and right injections.

Русский

Эквивалентность суммы и произведения раскладывает предобраз на пары произведений слева и справа.

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 piCongrLeft_preimage_univ_pi (f : ι' ≃ ι) (t : ∀ i, Set (α i)) :
    f.piCongrLeft α ⁻¹' univ.pi t = univ.pi fun i => t (f i) := by
  simpa [f.surjective.range_eq] using piCongrLeft_preimage_pi f univ t

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