monotone_mul_left_of_nonneg

Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic

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

English

If a ≥ 0, then the map x ↦ a*x is monotone.

Русский

Если a ≥ 0, то отображение x ↦ a*x монотонно.

LaTeX

$$$ a \\ge 0 \\Rightarrow \\operatorname{Monotone}(x \\mapsto a x) $$$

Lean4

theorem monotone_mul_left_of_nonneg [PosMulMono M₀] (ha : 0 ≤ a) : Monotone fun x ↦ a * x := fun _ _ h ↦
  mul_le_mul_of_nonneg_left h ha

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

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

Разделы

Аффилиация

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