monotone_smul_left_of_nonneg

Mathlib.Algebra.Order.Module.Defs

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

English

If a ≥ 0 and β is ordered, the map x ↦ a·x is monotone on β.

Русский

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

LaTeX

$$$a \\ge 0 \\Rightarrow \\ Monotone( x \\mapsto a\\cdot x ).$$$

Lean4

theorem monotone_smul_left_of_nonneg [PosSMulMono α β] (ha : 0 ≤ a) : Monotone ((a • ·) : β → β) :=
  PosSMulMono.smul_le_smul_of_nonneg_left ha

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

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

Разделы

Аффилиация

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