ennrealOfReal — Mathlib

English

If Real.HolderTriple p.toReal q.toReal r.toReal holds, then HolderTriple p q r holds in ENNReal.

Русский

Если Real.HolderTriple(p.toReal,q.toReal,r.toReal) выполняется, то HolderTriple p q r выполняется в ENNReal.

LaTeX

$$Real.HolderTriple p.toReal q.toReal r.toReal → HolderTriple p q r$$

Lean4

theorem _root_.Real.HolderTriple.ennrealOfReal {p q r : ℝ} (h : p.HolderTriple q r) :
    HolderTriple (ENNReal.ofReal p) (ENNReal.ofReal q) (ENNReal.ofReal r) := by
  simpa [holderTriple_iff, ofReal_inv_of_pos, h.pos, h.symm.pos, h.pos', ofReal_add, h.nonneg, h.symm.nonneg] using
    congr(ENNReal.ofReal $(h.inv_add_inv_eq_inv))

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