piCongrLeft_symm_preimage_univ_pi

English

A specialization of piCongrLeft_symm_preimage_pi to the universal product.

Русский

Специализация на единичный случай с универсальным произведением.

LaTeX

$$$$ (f.\\pi\\text{CongrLeft } α).symm^{-1}' \\mathrm{univ}.\\pi t = \\mathrm{univ}.\\pi t. $$$$

Lean4

theorem piCongrLeft_symm_preimage_univ_pi (f : ι' ≃ ι) (t : ∀ i, Set (α i)) :
    (f.piCongrLeft α).symm ⁻¹' univ.pi (fun i' => t <| f i') = univ.pi t := by
  simpa [f.surjective.range_eq] using piCongrLeft_symm_preimage_pi f univ t

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