piCongrLeft — Mathlib

English

There is an isometry between the space of maps i ↦ Y(i) and the space j ↦ Y(j) via e, given by e i.

Русский

Существует изометрия между пространством отображений i ↦ Y(i) и пространством j ↦ Y(j), заданная отображением e.

LaTeX

$$$ (\forall i, Y(i)) \simeq_i (\forall j, Y(j)) $$$

Lean4

/-- The natural isometry `∀ i, Y (e i) ≃ᵢ ∀ j, Y 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 (e i)) ≃ᵢ ∀ j, Y j :=
  (piCongrLeft' e.symm).symm

Похожие утверждения