instZero

Mathlib.Data.ENNReal.Holder

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

English

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

Русский

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

LaTeX

$$HolderTriple p 0 0$$

Lean4

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

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

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

Разделы

Аффилиация

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