div_le_iff

Mathlib.Data.ENNReal.Inv

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

← MathLib Explorer

English

If y ≠ 0 and y ≠ ∞, then x/y ≤ z iff x ≤ z·y.

Русский

Если y ≠ 0 и y ≠ ∞, то x/y ≤ z эквивалентно x ≤ z·y.

LaTeX

$$$y \neq 0 \land y \neq \infty \Rightarrow \dfrac{x}{y} \le z \iff x \le z \cdot y$$$

Lean4

protected theorem div_le_iff {x y z : ℝ≥0∞} (h1 : y ≠ 0) (h2 : y ≠ ∞) : x / y ≤ z ↔ x ≤ z * y := by
  rw [div_eq_mul_inv, ENNReal.mul_inv_le_iff h1 h2]

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

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

Разделы

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

Аффилиация

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