English
For p, q, r ∈ ENNReal with p.toNNReal > 0 and q.toNNReal > 0, NNReal.HolderTriple p.toNNReal q.toNNReal r.toNNReal holds if and only if HolderTriple p q r holds.
Русский
Для p, q, r ∈ ENNReal с p.toNNReal > 0 и q.toNNReal > 0 выполняется равенство: NNReal.HolderTriple p.toNNReal q.toNNReal r.toNNReal тогда и только тогда, когда HolderTriple p q r выполняется.
LaTeX
$$$NNReal.HolderTriple(p.toNNReal, q.toNNReal, r.toNNReal) \\iff HolderTriple(p, q, r)$$$
Lean4
theorem toNNReal_iff (hp : 0 < p.toNNReal) (hq : 0 < q.toNNReal) :
NNReal.HolderTriple p.toNNReal q.toNNReal r.toNNReal ↔ HolderTriple p q r :=
by
simp_rw [← NNReal.holderTriple_coe_iff, coe_toNNReal_eq_toReal]
apply toReal_iff r ?_ ?_
all_goals simpa [← coe_toNNReal_eq_toReal]
