isConjExponent_iff_eq_conjExponent

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#ENNReal.isConjExponent_iff_eq_conjExponent

← MathLib Explorer

English

For hp ≥ 1, p.HolderConjugate q ↔ q = 1 + (p - 1)⁻¹.

Русский

Для hp ≥ 1, p.HolderConjugate q ↔ q = 1 + (p - 1)⁻¹.

LaTeX

$$$p.HolderConjugate q \\iff q = 1 + (p - 1)^{-1}$$$

Lean4

theorem isConjExponent_iff_eq_conjExponent (hp : 1 ≤ p) : p.HolderConjugate q ↔ q = 1 + (p - 1)⁻¹ :=
  ⟨fun h ↦ h.conj_eq, by rintro rfl; exact .conjExponent hp⟩

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

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

Разделы

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

Аффилиация

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