toReal_iff — Mathlib

English

For hp>0 and hq>0, Real.HolderTriple p.toReal q.toReal r.toReal ↔ HolderTriple p q r.

Русский

При hp>0 и hq>0: Real.HolderTriple p.toReal q.toReal r.toReal ↔ HolderTriple p q r.

LaTeX

$$Real.HolderTriple p.toReal q.toReal r.toReal \\leftrightarrow HolderTriple p q r$$

Lean4

theorem toReal_iff (hp : 0 < p.toReal) (hq : 0 < q.toReal) :
    Real.HolderTriple p.toReal q.toReal r.toReal ↔ HolderTriple p q r :=
  by
  refine ⟨of_toReal, fun h ↦ ⟨?_, hp, hq⟩⟩
  rw [toReal_pos_iff] at hp hq
  simpa [toReal_add, Finiteness.inv_ne_top, hp.1.ne', hq.1.ne'] using congr(ENNReal.toReal $(h.inv_add_inv_eq_inv))

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