inv_one_sub_inv

Mathlib.Data.Real.ConjExponents

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

← MathLib Explorer

English

If 0 < a < 1, then a^{-1} and (1 − a)^{-1} are Holder conjugates.

Русский

Если 0 < a < 1, то a^{-1} и (1 − a)^{-1} являются сопряжёнными Холдером.

LaTeX

$$$0 < a < 1 \Rightarrow a^{-1} \HolderConjugate (1 - a)^{-1}$$$

Lean4

theorem inv_one_sub_inv (ha₀ : 0 < a) (ha₁ : a < 1) : a⁻¹.HolderConjugate (1 - a)⁻¹ :=
  holderConjugate_iff.mpr ⟨one_lt_inv₀ ha₀ |>.mpr ha₁, by simp⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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