English
Equivalence: reindexing a family by a bijection e yields a uniform isomorphism between the dependent product ∀i, β(e(i)) and ∀j, β(j).
Русский
Эквиваленция: переиндексирование семейства по биекцияe даёт равномерное изоморфизм между зависимым произведением ∀i, β(e(i)) и ∀j, β(j).
LaTeX
$$$\\bigl(\\forall i, \\beta(e(i))\\bigr) \\cong_{u} \\bigl(\\forall j, \\beta(j)\\bigr)$$$
Lean4
/-- `Equiv.piCongrLeft` as a uniform isomorphism: this is the natural isomorphism
`Π i, β (e i) ≃ᵤ Π j, β j` obtained from a bijection `ι ≃ ι'`. -/
@[simps toEquiv, simps! -isSimp apply]
def piCongrLeft {ι ι' : Type*} {β : ι' → Type*} [∀ j, UniformSpace (β j)] (e : ι ≃ ι') : (∀ i, β (e i)) ≃ᵤ ∀ j, β j
where
uniformContinuous_toFun :=
uniformContinuous_pi.mpr <|
e.forall_congr_right.mp fun i ↦ by
simpa only [Equiv.toFun_as_coe, Equiv.piCongrLeft_apply_apply] using Pi.uniformContinuous_proj _ i
uniformContinuous_invFun := Pi.uniformContinuous_precomp' _ e
toEquiv := Equiv.piCongrLeft _ e
