inv_one_sub_inv'

Mathlib.Data.Real.ConjExponents

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

English

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

Русский

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

LaTeX

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

Lean4

theorem inv_one_sub_inv' (ha : 1 ≤ a) : a.HolderConjugate (1 - a⁻¹)⁻¹ := by
  simpa using inv_one_sub_inv (ENNReal.inv_le_one.mpr ha)

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

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

Разделы

Аффилиация

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