piCongrRight_apply

Mathlib.LinearAlgebra.Pi

URI: https://scilib.ai/kg/mathlib#LinearEquiv.piCongrRight_apply

English

Uniformly apply a family of linear equivalences to a dependent function.

Русский

Единообразно применяем семейство линейных эквиваризций к зависимой функции.

LaTeX

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

Lean4

@[simp]
theorem piCongrRight_apply (e : (i : ι) → φ i ≃ₗ[R] ψ i) (f i) : piCongrRight e f i = e i (f i) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru