llcomp_apply

Mathlib.LinearAlgebra.BilinearMap

URI: https://scilib.ai/kg/mathlib#LinearMap.llcomp_apply

English

A variant of llcomp shows llcomp f g equals the standard composition f ∘ g.

Русский

Вариант llcomp показывает, что llcomp f g равен обычной композиции f ∘ g.

LaTeX

$$$$llcomp\ _{\cdot} (f) (g) = f \circ g.$$$$

Lean4

@[simp]
theorem llcomp_apply (f : N →ₛₗ[σ₂₃] P) (g : M →ₛₗ[σ₁₂] N) (x : M) : llcomp _ M N P f g x = f (g x) :=
  rfl

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

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

Разделы

Аффилиация

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