English
Equiv.piCongrRight provides a homeomorphism between the product of spaces Y1 i and Y2 i with F i homomorphisms.
Русский
Equiv.piCongrRight задает гомеоморфизм между продуктами пространств Y1 i и Y2 i с гомоморфизмами F i.
LaTeX
$$$ (\forall i, Y_1 i) \cong_{Top} (\forall i, Y_2 i) \quad\text{via } (F_i)_{i}. $$$
Lean4
/-- `Equiv.piCongrRight` as a homeomorphism: this is the natural homeomorphism
`Π i, Y₁ i ≃ₜ Π j, Y₂ i` obtained from homeomorphisms `Y₁ i ≃ₜ Y₂ i` for each `i`. -/
@[simps! apply toEquiv]
def piCongrRight {ι : Type*} {Y₁ Y₂ : ι → Type*} [∀ i, TopologicalSpace (Y₁ i)] [∀ i, TopologicalSpace (Y₂ i)]
(F : ∀ i, Y₁ i ≃ₜ Y₂ i) : (∀ i, Y₁ i) ≃ₜ ∀ i, Y₂ i
where
continuous_toFun := Pi.continuous_postcomp' fun i ↦ (F i).continuous
continuous_invFun := Pi.continuous_postcomp' fun i ↦ (F i).symm.continuous
toEquiv := Equiv.piCongrRight fun i => (F i).toEquiv
