mulLeftMono

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#NNReal.mulLeftMono

English

Multiplication by a nonnegative NNReal on the left is monotone: if a ≤ b then c · a ≤ c · b.

Русский

Умножение слева на неотрицательное NNReal монотонно: если a ≤ b, то c·a ≤ c·b.

LaTeX

$$$ \\forall a,b,c \\in \\mathbb{R}_{\\ge 0}, a \\le b \\Rightarrow c a \\le c b. $$$

Lean4

instance mulLeftMono : MulLeftMono ℝ≥0 :=
  inferInstance

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

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

Разделы

Аффилиация

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