one_div_add_one_div

Mathlib.Data.Real.ConjExponents

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

English

Let p, q, r real with p.HolderTriple q r. Then 1/p + 1/q = 1/r.

Русский

Пусть p, q, r вещественные, удовлетворяющие p.HolderTriple q r. Тогда 1/p + 1/q = 1/r.

LaTeX

$$$ p.HolderTriple q r \rightarrow \frac{1}{p} + \frac{1}{q} = \frac{1}{r} $$$

Lean4

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

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

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

Разделы

Аффилиация

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