compL_apply

Mathlib.Analysis.Normed.Operator.Bilinear

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.compL_apply

English

For linear maps f and g, the composition operator satisfies compL(f,g) = f ∘ g.

Русский

Для линейных отображений f и g выполняется compL(f,g) = f ∘ g.

LaTeX

$$$\operatorname{compL}(f,g) = f \circ g$$$

Lean4

@[simp]
theorem compL_apply (f : Fₗ →L[𝕜] Gₗ) (g : E →L[𝕜] Fₗ) : compL 𝕜 E Fₗ Gₗ f g = f.comp g :=
  rfl

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

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

Разделы

Аффилиация

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