English
There is a natural isometry between the product (∀ i, Y i) and (∀ j, Y (e.symm j)) induced by a bijection e: ι ≃ ι' between finite index sets.
Русский
Существует естественная изометрия между произведениями (∀ i, Y_i) и (∀ j, Y_(e.symm j)), индукированная биекцией e: ι ≃ ι' между конечными множествами индексов.
LaTeX
$$$ (\forall i, Y_i) \simeq_i (\forall j, Y_{e^{-1}(j)}) $$$
Lean4
/-- The natural isometry `∀ i, Y i ≃ᵢ ∀ j, Y (e.symm j)` obtained from a bijection `ι ≃ ι'` of
fintypes. `Equiv.piCongrLeft'` as an `IsometryEquiv`. -/
@[simps!]
def piCongrLeft' {ι' : Type*} [Fintype ι] [Fintype ι'] {Y : ι → Type*} [∀ j, PseudoEMetricSpace (Y j)] (e : ι ≃ ι') :
(∀ i, Y i) ≃ᵢ ∀ j, Y (e.symm j) where
toEquiv := Equiv.piCongrLeft' _ e
isometry_toFun x1
x2 := by
simp_rw [edist_pi_def, Finset.sup_univ_eq_iSup]
exact (Equiv.iSup_comp (g := fun b ↦ edist (x1 b) (x2 b)) e.symm)
