lineMap_mono_left

Mathlib.LinearAlgebra.AffineSpace.Ordered

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

← MathLib Explorer

English

In an ordered setting, if a ≤ a' and r ≤ 1, then lineMap(a,b,r) ≤ lineMap(a',b,r).

Русский

В упорядоченном окружении, если a ≤ a' и r ≤ 1, то lineMap(a,b,r) ≤ lineMap(a',b,r).

LaTeX

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

Lean4

theorem lineMap_mono_left (ha : a ≤ a') (hr : r ≤ 1) : lineMap a b r ≤ lineMap a' b r :=
  by
  simp only [lineMap_apply_module]
  gcongr
  exact sub_nonneg.2 hr

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

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

Разделы

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

Аффилиация

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