inv_sub_one

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#Real.HolderConjugate.inv_sub_one

English

If p and q are Holder conjugates, then p^{-1} − 1 = − q^{-1}.

Русский

Если p и q сопряжены Холдером, то p^{-1} − 1 = − q^{-1}.

LaTeX

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

Lean4

theorem inv_sub_one : p⁻¹ - 1 = -q⁻¹ := by simpa using congr(-$(h.one_sub_inv))

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

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

Разделы

Аффилиация

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