le

Mathlib.Data.ENNReal.Holder

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

English

Let p, q, r in ENNReal satisfy the HolderTriple relation p, q, r. Then r is at most p: r ≤ p.

Русский

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

LaTeX

$$$HolderTriple(p,q,r) \Rightarrow r \le p$$$

Lean4

theorem le : r ≤ p := by simp [← ENNReal.inv_le_inv, ← @inv_inv_add_inv p q r, inv_inv]

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

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

Разделы

Аффилиация

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