prod_apply

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

Applying the product to p yields the pair of values (f(p), g(p)).

Русский

Применение произведения к p даёт пару значений (f(p), g(p)).

LaTeX

$$$\\mathrm{prod}(f,g)(p) = (f(p), g(p))$$$

Lean4

@[simp]
theorem prod_apply (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3) (p : P1) : prod f g p = (f p, g p) :=
  rfl

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

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

Разделы

Аффилиация

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