lineMap_mono_right

Mathlib.LinearAlgebra.AffineSpace.Ordered

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

English

If a ≤ a', b ≤ b', and r ∈ [0,1], then lineMap(a,b,r) ≤ lineMap(a',b',r).

Русский

Если a ≤ a', b ≤ b', и 0 ≤ r ≤ 1, тогда lineMap(a,b,r) ≤ lineMap(a',b',r).

LaTeX

$$$ lineMap\ a\ b\ r \le \ lineMap\ a'\ b'\ r $$$

Lean4

theorem lineMap_mono_right (hb : b ≤ b') (hr : 0 ≤ r) : lineMap a b r ≤ lineMap a b' r :=
  by
  simp only [lineMap_apply_module]
  gcongr

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

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

Разделы

Аффилиация

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