lineMap_same

Mathlib.LinearAlgebra.AffineSpace.AffineMap

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

English

The line map is symmetric up to precomposing with the origin-swap map.

Русский

LineMap симметрично относительно перестановки начала и конца прямой.

LaTeX

$$$\text{lineMap}(p_0,p_1) = (\text{lineMap}(p_1,p_0)).\mathrm{comp}(\text{lineMap}(1,0))$$$

Lean4

@[simp]
theorem lineMap_same (p : P1) : lineMap p p = const k k p :=
  ext <| lineMap_same_apply p

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

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

Разделы

Аффилиация

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