lineMap_apply

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

The evaluation rule for lineMap gives the explicit formula for any scalar input.

Русский

Правило вычисления lineMap задаёт явную формулу для любого входного скаляра.

LaTeX

$$$ lineMap(p_0,p_1)(c) = c \cdot (p_1 - p_0) + p_0 $$$

Lean4

theorem lineMap_apply (p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ c = c • (p₁ -ᵥ p₀) +ᵥ p₀ :=
  rfl

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

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

Разделы

Аффилиация

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