English
Equiv.piCongr composes a bijection of indices with a family of homeomorphisms to yield a homeomorphism between two dependent products.
Русский
Equiv.piCongr комбинирует биекцию индексов с семейством гомеоморфизмов, получая гомеоморфизм между зависимыми произведениями.
LaTeX
$$$\text{piCongr}\ e\ F : (\forall i, Y_1 i) \cong_{Top} (\forall i', Y_2 i').$$$
Lean4
/-- `Equiv.piCongr` as a homeomorphism: this is the natural homeomorphism
`Π i₁, Y₁ i ≃ₜ Π i₂, Y₂ i₂` obtained from a bijection `ι₁ ≃ ι₂` and homeomorphisms
`Y₁ i₁ ≃ₜ Y₂ (e i₁)` for each `i₁ : ι₁`. -/
@[simps! apply toEquiv]
def piCongr {ι₁ ι₂ : Type*} {Y₁ : ι₁ → Type*} {Y₂ : ι₂ → Type*} [∀ i₁, TopologicalSpace (Y₁ i₁)]
[∀ i₂, TopologicalSpace (Y₂ i₂)] (e : ι₁ ≃ ι₂) (F : ∀ i₁, Y₁ i₁ ≃ₜ Y₂ (e i₁)) : (∀ i₁, Y₁ i₁) ≃ₜ ∀ i₂, Y₂ i₂ :=
(Homeomorph.piCongrRight F).trans (Homeomorph.piCongrLeft e)
