lineMap_apply_module

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

← MathLib Explorer

English

In the vector setting, the line map is the affine combination as above.

Русский

Векторный контекст: линия через p0 и p1 выражается как аффинная комбинация.

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 = (1 - c) • p₀ + c • p₁ := by
  simp [lineMap_apply_module', smul_sub, sub_smul]; abel

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

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

Разделы

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

Аффилиация

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