smul_nonneg'

Mathlib.Algebra.Order.Module.Defs

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

← MathLib Explorer

English

If a ≥ 0 and b ≥ 0 and SMulWithZero is present, then a • b ≥ 0.

Русский

Если a ≥ 0 и b ≥ 0 и присутствует SMulWithZero, тогда a • b ≥ 0.

LaTeX

$$0 \\le a \\Rightarrow 0 \\le b \\Rightarrow 0 \\le a \\cdot b$$

Lean4

theorem smul_nonneg' [SMulPosMono α β] (ha : 0 ≤ a) (hb : 0 ≤ b₁) : 0 ≤ a • b₁ := by
  simpa only [zero_smul] using smul_le_smul_of_nonneg_right ha hb

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

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

Разделы

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

Аффилиация

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