piCongrLeft — Mathlib

English

The action of piCongrRight on a function is pointwise: (piCongrRight e) f i = e_i(f_i).

Русский

Действие piCongrRight на функцию есть по точкам: (piCongrRight e) f i = e_i (f_i).

LaTeX

$$$$ (\\pi\\mathrm{CongrRight}\\,e)\\,f\\,i = e_i\\,(f_i). $$$$

Lean4

/-- Transporting dependent functions through an equivalence of the base,
expressed as a "simplification".

This is `Equiv.piCongrLeft` as a `LinearEquiv` -/
def piCongrLeft (e : ι' ≃ ι) : ((i' : ι') → φ (e i')) ≃ₗ[R] (i : ι) → φ i :=
  (piCongrLeft' R φ e.symm).symm

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