comp_apply

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.comp_apply

← MathLib Explorer

English

For all p ∈ P1, (f ∘ g)(p) = f(g(p)).

Русский

Для всех p ∈ P1 выполняется (f ∘ g)(p) = f(g(p)).

LaTeX

$$$ (f.comp\, g)\, p = f\\,(g\\, p) $$$

Lean4

/-- Composition of affine maps acts as applying the two functions. -/
theorem comp_apply (f : P2 →ᵃ[k] P3) (g : P1 →ᵃ[k] P2) (p : P1) : f.comp g p = f (g p) :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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