lt_inv_iff_mul_lt

Mathlib.Data.NNReal.Defs

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

← MathLib Explorer

English

For r,p ∈ ℝ≥0 with p ≠ 0, r < p⁻¹ ↔ r p < 1.

Русский

Для r,p ∈ ℝ≥0, p ≠ 0, верно r < p⁻¹ ↔ r p < 1.

LaTeX

$$$\forall r,p \in \mathbb{R}_{\ge 0},\ p \neq 0\Rightarrow r < p^{-1} \iff r p < 1$$$

Lean4

@[simp]
theorem lt_inv_iff_mul_lt {r p : ℝ≥0} (h : p ≠ 0) : r < p⁻¹ ↔ r * p < 1 := by
  rw [← mul_lt_mul_iff_right₀ (pos_iff_ne_zero.2 h), mul_inv_cancel₀ h, mul_comm]

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

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

Разделы

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

Аффилиация

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