conj_eq

Mathlib.Data.Real.ConjExponents

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

English

conjExponent_eq: conjExponent p = q when HolderConjugate p q.

Русский

conjExponent_eq: conjExponent p = q, если HolderConjugate p q.

LaTeX

$$$conjExponent(p) = q$$$

Lean4

theorem conj_eq : q = 1 + (p - 1)⁻¹ :=
  conjExponent_eq.symm

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

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

Разделы

Аффилиация

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