div_lt_one_of_lt

Mathlib.Data.NNReal.Defs

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

English

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

Русский

Если a < b для a,b ∈ ℝ≥0, то a / b < 1.

LaTeX

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

Lean4

theorem div_lt_one_of_lt {a b : ℝ≥0} (h : a < b) : a / b < 1 := by rwa [div_lt_iff₀ h.bot_lt, one_mul]

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

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

Разделы

Аффилиация

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