inv_inv_add_inv

Mathlib.Data.ENNReal.Holder

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

English

If p,q,r form a HolderTriple, then (p^{-1} + q^{-1})^{-1} = r.

Русский

Если p,q,r образуют HolderTriple, то (p^{-1} + q^{-1})^{-1} = r.

LaTeX

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

Lean4

theorem inv_inv_add_inv : (p⁻¹ + q⁻¹)⁻¹ = r := by simp [inv_add_inv_eq_inv p q r]

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

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

Разделы

Аффилиация

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