of_toNNReal — Mathlib

English

Let p, q, r be extended nonnegative real numbers. If the NNReal reductions p.toNNReal, q.toNNReal, r.toNNReal form a Holder triple, then p, q, r form a Holder triple.

Русский

Пусть p, q, r принадлежат расширенным неотрицательным числам. Если их образы в NNReal через toNNReal образуют тройку Holder, то и p, q, r образуют тройку Holder.

LaTeX

$$$NNReal.HolderTriple(p.toNNReal, q.toNNReal, r.toNNReal) \\Rightarrow HolderTriple(p, q, r)$$$

Lean4

theorem of_toNNReal (h : NNReal.HolderTriple p.toNNReal q.toNNReal r.toNNReal) : HolderTriple p q r :=
  .of_toReal <| by simpa only [coe_toNNReal_eq_toReal] using h.coe

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