of_toReal — Mathlib

English

From Real.HolderTriple p q r, obtain ENNReal.HolderTriple (ENNReal.ofReal p) (ENNReal.ofReal q) (ENNReal.ofReal r).

Русский

Из Real.HolderTriple p q r следует ENNReal.HolderTriple (ENNReal.ofReal p) (ENNReal.ofReal q) (ENNReal.ofReal r).

LaTeX

$$Real.HolderTriple p q r → HolderTriple (ENNReal.ofReal p) (ENNReal.ofReal q) (ENNReal.ofReal r)$$

Lean4

theorem of_toReal (h : Real.HolderTriple p.toReal q.toReal r.toReal) : HolderTriple p q r :=
  by
  have hp := h.pos
  have hq := h.symm.pos
  have hr := h.pos'
  rw [toReal_pos_iff] at hp hq hr
  simpa [hp.2.ne, hq.2.ne, hr.2.ne] using h.ennrealOfReal

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