le_inv_iff_mul_le

Mathlib.Data.NNReal.Defs

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

← 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 \le p^{-1} \iff r p \le 1$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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