one_sub_inv

Mathlib.Data.ENNReal.Holder

URI: https://scilib.ai/kg/mathlib#ENNReal.HolderConjugate.one_sub_inv

English

For HolderConjugate p q, one minus p⁻¹ equals q⁻¹.

Русский

Для HolderConjugate p q: 1 − p⁻¹ = q⁻¹.

LaTeX

$$HolderConjugate p q \Rightarrow 1 - p^{-1} = q^{-1}$$

Lean4

theorem one_sub_inv : 1 - p⁻¹ = q⁻¹ :=
  @inv_one ℝ≥0∞ _ ▸ HolderTriple.inv_sub_inv_eq_inv q p one_ne_zero

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

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

Разделы

Аффилиация

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