vadd_contLinear

Mathlib.Topology.Algebra.ContinuousAffineMap

URI: https://scilib.ai/kg/mathlib#ContinuousAffineMap.vadd_contLinear

English

The contLinear component respects vadd: (f +ᵥ g).contLinear = f.contLinear + g.contLinear.

Русский

Составной contLinear при сумме через vadd равен сумме contLinear: (f +ᵥ g).contLinear = f.contLinear + g.contLinear.

LaTeX

$$$$(f +\\!_v g).contLinear = f.contLinear + g.contLinear.$$$$

Lean4

@[simp]
theorem vadd_contLinear (f : P →ᴬ[R] W) (g : P →ᴬ[R] Q) : (f +ᵥ g).contLinear = f.contLinear + g.contLinear :=
  rfl

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

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

Разделы

Аффилиация

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