inv_le_inv

Mathlib.Data.ENNReal.Holder

URI: https://scilib.ai/kg/mathlib#ENNReal.HolderTriple.inv_le_inv

English

Let p, q, r ∈ ENNReal satisfy HolderTriple p q r. Then p⁻¹ ≤ r⁻¹.

Русский

Пусть p, q, r ∈ ℝ≥0∞ удовлетворяют HolderTriple p q r. Тогда p⁻¹ ≤ r⁻¹.

LaTeX

$$$HolderTriple(p,q,r) \Rightarrow p^{-1} \le r^{-1}$$$

Lean4

protected theorem inv_le_inv : p⁻¹ ≤ r⁻¹ := by simp [ENNReal.inv_le_inv, le p q r]

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

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

Разделы

Аффилиация

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