one_div_eq

Mathlib.Data.ENNReal.Holder

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

English

For a HolderTriple p,q,r, 1/r = 1/p + 1/q.

Русский

Для HolderTriple p,q,r, 1/r = 1/p + 1/q.

LaTeX

$$1/r = 1/p + 1/q$$

Lean4

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

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

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

Разделы

Аффилиация

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