one_sub_inv_inv

Mathlib.Data.Real.ConjExponents

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

English

Theorem one_sub_inv_inv (ha : a ≤ 1) : (1 - a)⁻¹.HolderConjugate a⁻¹.

Русский

Теорема one_sub_inv_inv (ha : a ≤ 1) : (1 - a)⁻¹.HolderConjugate a⁻¹.

LaTeX

$$$(1 - a)^{-1}.HolderConjugate(a^{-1})$$$

Lean4

theorem one_sub_inv_inv (ha : a ≤ 1) : (1 - a)⁻¹.HolderConjugate a⁻¹ :=
  (inv_one_sub_inv ha).symm

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

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

Разделы

Аффилиация

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