toNNReal — Mathlib

English

If hp > 0 and hq > 0, and [HolderTriple p q r] holds, then NNReal.HolderTriple p.toNNReal q.toNNReal r.toNNReal holds.

Русский

Пусть hp > 0 и hq > 0, и выполняется [HolderTriple p q r]. Тогда NNReal.HolderTriple p.toNNReal q.toNNReal r.toNNReal выполняется.

LaTeX

$$$NNReal.HolderTriple(p.toNNReal, q.toNNReal, r.toNNReal)$$$

Lean4

theorem toNNReal (hp : 0 < p.toNNReal) (hq : 0 < q.toNNReal) [HolderTriple p q r] :
    NNReal.HolderTriple p.toNNReal q.toNNReal r.toNNReal :=
  toNNReal_iff r hp hq |>.mpr ‹_›

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