map_vadd

Mathlib.Topology.Algebra.ContinuousAffineMap

URI: https://scilib.ai/kg/mathlib#ContinuousAffineMap.map_vadd

English

The affine part of the lineMap coincides with the standard lineMap from Affine geometry.

Русский

Аффинная часть lineMap совпадает с стандартной lineMap в аффинной геометрии.

LaTeX

$$$ (\text{lineMap}(p_0,p_1)).toAffineMap = \text{AffineMap.lineMap }(k:=R)\ p_0\ p_1 $$$

Lean4

@[simp]
theorem map_vadd (f : P →ᴬ[R] Q) (p : P) (v : V) : f (v +ᵥ p) = f.contLinear v +ᵥ f p :=
  f.map_vadd' p v

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

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

Разделы

Аффилиация

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