of_pos

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#NNReal.HolderTriple.of_pos

← MathLib Explorer

English

For p,q > 0, HolderTriple p q (p^{-1} + q^{-1})^{-1} holds.

Русский

Для p,q > 0 выполняется HolderTriple p q (p^{-1} + q^{-1})^{-1}.

LaTeX

$$$p>0 \land q>0 \Rightarrow HolderTriple p q (p^{-1} + q^{-1})^{-1}$$$

Lean4

theorem of_pos (hp : 0 < p) (hq : 0 < q) : HolderTriple p q (p⁻¹ + q⁻¹)⁻¹
    where
  inv_add_inv_eq_inv := inv_inv _ |>.symm
  left_pos := hp
  right_pos := hq

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

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

Разделы

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

Аффилиация

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