instInfty

Mathlib.Data.ENNReal.Holder

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

English

For any p ∈ ENNReal, the triple (p, ∞, p) satisfies HolderTriple.

Русский

Для любого p ∈ ENNReal тройка (p, ∞, p) удовлетворяет HolderTriple.

LaTeX

$$HolderTriple p ∞ p$$

Lean4

instance instInfty (p : ℝ≥0∞) : HolderTriple p ∞ p where inv_add_inv_eq_inv := by simp

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

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

Разделы

Аффилиация

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