mul_lt_of_lt_div

Mathlib.Data.NNReal.Defs

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

← MathLib Explorer

English

If a < b / r for a,b,r ∈ ℝ≥0, then a r < b.

Русский

Если a < b / r, то a r < b.

LaTeX

$$$\forall a,b,r \in \mathbb{R}_{\ge 0},\ a < \dfrac{b}{r}\Rightarrow a r < b$$$

Lean4

theorem mul_lt_of_lt_div {a b r : ℝ≥0} (h : a < b / r) : a * r < b :=
  (lt_div_iff₀ <| pos_iff_ne_zero.2 fun hr => False.elim <| by simp [hr] at h).1 h

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

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

Разделы

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

Аффилиация

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