ennrealOfReal — Mathlib

English

If Real p H q, then p.toNNReal.HolderConjugate q.toNNReal.

Русский

Если p и q — сопряжённые Холдера в Real, то их преобразования в NNReal сохраняют сопряжённость.

LaTeX

$$Real.HolderConjugate p q → (p.toNNReal).HolderConjugate (q.toNNReal)$$

Lean4

theorem _root_.Real.HolderConjugate.ennrealOfReal {p q : ℝ} (h : p.HolderConjugate q) :
    HolderConjugate (ENNReal.ofReal p) (ENNReal.ofReal q) := by simpa using Real.HolderTriple.ennrealOfReal h

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