proj_linear — Mathlib

English

Applying lineMap inside a family indexed by i commutes with evaluating at i: pi_lineMap_apply

Русский

Применение lineMap внутри семейства, индексируемого i, коммутирует с вычислением по индексу i.

LaTeX

$$$ (\\text{pi_lineMap_apply})\\, (f,g,c,i) : lineMap_f_g_c_i = lineMap_{i}(f_i, g_i, c) $$$

Lean4

@[simp]
theorem proj_linear (i : ι) : (@proj k _ ι V P _ _ _ i).linear = @LinearMap.proj k ι _ V _ _ i :=
  rfl

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