lineMap_one_half

Mathlib.LinearAlgebra.AffineSpace.MidpointZero

URI: https://scilib.ai/kg/mathlib#lineMap_one_half

← MathLib Explorer

English

Similarly, lineMap a b at parameter 1/2 equals the midpoint of a and b.

Русский

Аналогично, lineMap(a,b,1/2) равно середине между a и b.

LaTeX

$$$ lineMap\ a\ b\ (1/2) = midpoint\ k\ a\ b $$$

Lean4

theorem lineMap_one_half {R : Type*} {V P : Type*} [DivisionRing R] [CharZero R] [AddCommGroup V] [Module R V]
    [AddTorsor V P] (a b : P) : lineMap a b (1 / 2 : R) = midpoint R a b := by rw [one_div, lineMap_inv_two]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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