English
Equiv piCongr provides a uniform isomorphism between Π i, β_i and Π j, β_j given a bijection e and a collection of uniform isomorphisms F_i: β_i ≃ᵤ β_{e(i)}.
Русский
Equiv piCongr обеспечивает равномерный изоморфизм между Π_i β_i и Π_j β_j, dada биекция e и набор равномерных изоморфизмов F_i: β_i ≃ᵤ β_{e(i)}.
LaTeX
$$$(\\forall i\\in I, \\beta_i) \\cong_{u} (\\forall j\\in J, \\beta_j)$$$
Lean4
/-- `Equiv.piCongr` as a uniform isomorphism: this is the natural isomorphism
`Π i₁, β₁ i ≃ᵤ Π i₂, β₂ i₂` obtained from a bijection `ι₁ ≃ ι₂` and isomorphisms
`β₁ i₁ ≃ᵤ β₂ (e i₁)` for each `i₁ : ι₁`. -/
@[simps! apply toEquiv]
def piCongr {ι₁ ι₂ : Type*} {β₁ : ι₁ → Type*} {β₂ : ι₂ → Type*} [∀ i₁, UniformSpace (β₁ i₁)]
[∀ i₂, UniformSpace (β₂ i₂)] (e : ι₁ ≃ ι₂) (F : ∀ i₁, β₁ i₁ ≃ᵤ β₂ (e i₁)) : (∀ i₁, β₁ i₁) ≃ᵤ ∀ i₂, β₂ i₂ :=
(UniformEquiv.piCongrRight F).trans (UniformEquiv.piCongrLeft e)
