Theorems · Theorem · real analysis
ENNReal.HolderTriple.toNNReal
∀ {p q : ENNReal} (r : ENNReal),
0 < p.toNNReal → 0 < q.toNNReal → ∀ [p.HolderTriple q r], p.toNNReal.HolderTriple q.toNNReal r.toNNReal- Defined in
- Mathlib.Data.Real.ConjExponents
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 136 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- ENNReal.HolderTriple
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- ENNRealstatement and proof · cited by 9,879
- NNRealstatement · cited by 4,310
- ENNReal.toNNRealstatement and proof · cited by 165
- ENNReal.HolderTriplestatement and proof · cited by 65
- NNReal.HolderTriplestatement · cited by 42
- ENNReal.HolderTriple.toNNReal_iffproof · cited by 1
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.