of_toNNReal

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#ENNReal.HolderConjugate.of_toNNReal

← MathLib Explorer

English

If h : NNReal.HolderConjugate p.toNNReal q.toNNReal holds, then p.HolderConjugate q holds.

Русский

Если h : NNReal.HolderConjugate p.toNNReal q.toNNReal, то p.HolderConjugate q держится.

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru