lineMap_apply_module'

Mathlib.LinearAlgebra.AffineSpace.AffineMap

URI: https://scilib.ai/kg/mathlib#AffineMap.lineMap_apply_module'

English

In the vector setting, lineMap takes a scalar c and returns the affine combination c(p1−p0) + p0.

Русский

Векторное lineMap задаёт линейную комбинацию c(p1−p0)+p0.

LaTeX

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

Lean4

theorem lineMap_apply_module' (p₀ p₁ : V1) (c : k) : lineMap p₀ p₁ c = c • (p₁ - p₀) + p₀ :=
  rfl

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

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

Разделы

Аффилиация

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