fst_lineMap

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

LineMap with identical endpoints collapses to the constant map at that point.

Русский

LineMap с одинаковыми концами сводится к константному отображению в точку.

LaTeX

$$$ lineMap(p,p)(c) = p $$$

Lean4

@[simp]
theorem fst_lineMap (p₀ p₁ : P1 × P2) (c : k) : (lineMap p₀ p₁ c).1 = lineMap p₀.1 p₁.1 c :=
  fst.apply_lineMap p₀ p₁ c

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

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

Разделы

Аффилиация

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