smul_nonneg

Mathlib.Algebra.Order.Module.Defs

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

English

If a ≥ 0 and b ≥ 0 and the action is monotone, then a • b ≥ 0.

Русский

Если a ≥ 0 и b ≥ 0 и действие монотонно, то a • b ≥ 0.

LaTeX

$$0 \\le a \\Rightarrow 0 \\le b_1 \\Rightarrow 0 \\le a \\cdot b_1$$

Lean4

theorem smul_nonneg [PosSMulMono α β] (ha : 0 ≤ a) (hb : 0 ≤ b₁) : 0 ≤ a • b₁ := by
  simpa only [smul_zero] using smul_le_smul_of_nonneg_left hb ha

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

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

Разделы

Аффилиация

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