mul_lt_mul

Mathlib.Data.ENNReal.Operations

URI: https://scilib.ai/kg/mathlib#ENNReal.mul_lt_mul

English

If a < c and b < d then a * b < c * d in ENNReal.

Русский

Если a < c и b < d, то a·b < c·d в ENNReal.

LaTeX

$$$a < c \rightarrow b < d \rightarrow a \cdot b < c \cdot d$$$

Lean4

@[mono, gcongr]
theorem mul_lt_mul (ac : a < c) (bd : b < d) : a * b < c * d :=
  WithTop.mul_lt_mul ac bd

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

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

Разделы

Аффилиация

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