one_div_eq

Mathlib.Data.Real.ConjExponents

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

English

Equivalently, 1/r = 1/p + 1/q for HolderTriple p q r.

Русский

Эквивалентно, 1/r = 1/p + 1/q при тройке Холдера p q r.

LaTeX

$$$r^{-1} = p^{-1} + q^{-1}$$$

Lean4

theorem one_div_eq : 1 / r = 1 / p + 1 / q :=
  h.one_div_add_one_div.symm

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

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

Разделы

Аффилиация

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