piCongrLeft' — Mathlib

English

A linear equivalence implementing left-transport of dependent functions along an equivalence of index types.

Русский

Линейное эквивалентное отображение, реализующее левосторонний перенос зависимых функций вдоль эквиваленции индексов.

LaTeX

$$$$\\text{piCongrLeft'}(e) : ((i' : ι) \\to φ (e i')) \\simeq_l ((i : ι) \\to φ i). $$$$

Lean4

/-- Transport dependent functions through an equivalence of the base space.

This is `Equiv.piCongrLeft'` as a `LinearEquiv`. -/
@[simps +simpRhs]
def piCongrLeft' (e : ι ≃ ι') : ((i' : ι) → φ i') ≃ₗ[R] (i : ι') → φ <| e.symm i :=
  { Equiv.piCongrLeft' φ e with
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }

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