apply_lineMap

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

Affine maps preserve the line parametrization under composition.

Русский

Аффинное отображение сохраняет параметризацию прямой под композицию.

LaTeX

$$$ f(\text{lineMap}(p_0,p_1)(c)) = \text{lineMap}(f p_0, f p_1)(c) $$$

Lean4

@[simp]
theorem apply_lineMap (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k) : f (lineMap p₀ p₁ c) = lineMap (f p₀) (f p₁) c := by
  simp [lineMap_apply]

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

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

Разделы

Аффилиация

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