toNNReal_iff — Mathlib

English

For hp > 1, NNReal.HolderConjugate p.toNNReal q.toNNReal ↔ HolderConjugate p q.

Русский

Для hp > 1, NNReal.HolderConjugate p.toNNReal q.toNNReal эквивалентно HolderConjugate p q.

LaTeX

$$$NNReal.HolderConjugate(p.toNNReal, q.toNNReal) \\iff HolderConjugate(p, q)$$$

Lean4

theorem toNNReal_iff (hp : 1 < p.toNNReal) : NNReal.HolderConjugate p.toNNReal q.toNNReal ↔ HolderConjugate p q :=
  by
  simp_rw [← NNReal.holderTriple_coe_iff, coe_toNNReal_eq_toReal]
  apply toReal_iff ?_
  all_goals simpa [← coe_toNNReal_eq_toReal]

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