lineMap_mono_endpoints

Mathlib.LinearAlgebra.AffineSpace.Ordered

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

← MathLib Explorer

English

LineMap with parameter 1/2 equals the midpoint.

Русский

LineMap с параметром 1/2 равен середине.

LaTeX

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

Lean4

theorem lineMap_mono_endpoints (ha : a ≤ a') (hb : b ≤ b') (h₀ : 0 ≤ r) (h₁ : r ≤ 1) :
    lineMap a b r ≤ lineMap a' b' r :=
  (lineMap_mono_left ha h₁).trans (lineMap_mono_right hb h₀)

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

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

Разделы

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

Аффилиация

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