one_div_add_one_div

Mathlib.Data.ENNReal.Holder

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

English

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

Русский

Для HolderTriple p,q,r верно 1/p + 1/q = 1/r.

LaTeX

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

Lean4

theorem one_div_add_one_div : 1 / p + 1 / q = 1 / r := by simpa using inv_add_inv_eq_inv ..

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

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

Разделы

Аффилиация

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