symm

Mathlib.Data.ENNReal.Holder

URI: https://scilib.ai/kg/mathlib#ENNReal.HolderTriple.symm

← MathLib Explorer

English

If p,q,r form a HolderTriple, then q,p,r also forms a HolderTriple.

Русский

Если p,q,r образуют HolderTriple, то q,p,r тоже образуют HolderTriple.

LaTeX

$$HolderTriple q p r$$

Lean4

instance symm {p q r : ℝ≥0∞} [hpqr : HolderTriple p q r] : HolderTriple q p r where
  inv_add_inv_eq_inv := add_comm p⁻¹ q⁻¹ ▸ hpqr.inv_add_inv_eq_inv

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

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

Разделы

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

Аффилиация

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