piCongrLeft_symm_preimage_pi — Mathlib

English

In a change of indices by an equivalence f, the symmetric preimage of a product decomposes as the product over the image under f.

Русский

При замене индексов эквивалентностью f симметричное предобразование произведения распадается на произведение по образу под f.

LaTeX

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

Lean4

theorem piCongrLeft_symm_preimage_pi (f : ι' ≃ ι) (s : Set ι') (t : ∀ i, Set (α i)) :
    (f.piCongrLeft α).symm ⁻¹' s.pi (fun i' => t <| f i') = (f '' s).pi t := by ext; simp

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