English
Equiv.piCongrLeft is a natural homeomorphism induced by a bijection on indices for a family of spaces.
Русский
Equiv.piCongrLeft — естественный гомеоморфизм, индуцируемый биекцией на индексах для семейства пространств.
LaTeX
$$$ {\iota \ \iota'} \ {Y : a \to Type*} [\forall j, TopologicalSpace (Y j)] (e : \iota \simeq \iota') : (\forall i, Y (e i)) \cong_{\mathrm{Top}} \forall j, Y j.$$$
Lean4
/-- `Equiv.piCongrLeft` as a homeomorphism: this is the natural homeomorphism
`Π i, Y (e i) ≃ₜ Π j, Y j` obtained from a bijection `ι ≃ ι'`. -/
@[simps +simpRhs toEquiv, simps! -isSimp apply]
def piCongrLeft {ι ι' : Type*} {Y : ι' → Type*} [∀ j, TopologicalSpace (Y j)] (e : ι ≃ ι') : (∀ i, Y (e i)) ≃ₜ ∀ j, Y j
where
continuous_toFun :=
continuous_pi <|
e.forall_congr_right.mp fun i ↦ by
simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using continuous_apply i
continuous_invFun := Pi.continuous_precomp' e
toEquiv := Equiv.piCongrLeft _ e
