lineMap_apply_one

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

The line map starts at p0 when the parameter is 0.

Русский

Линейная карта начинается в p0, когда параметр равен 0.

LaTeX

$$$ lineMap(p_0,p_1)(0) = p_0 $$$

Lean4

@[simp]
theorem lineMap_apply_one (p₀ p₁ : P1) : lineMap p₀ p₁ (1 : k) = p₁ := by simp [lineMap_apply]

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

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

Разделы

Аффилиация

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