symm

Mathlib.Data.Real.ConjExponents

URI: https://scilib.ai/kg/mathlib#NNReal.HolderConjugate.symm

English

HolderConjugate relation is symmetric: if p is conjugate to q, then q is conjugate to p.

Русский

Отношение конъюгирования Холдера симметрично: если p конъугирован с q, то q конъугирован с p.

LaTeX

$$$\operatorname{HolderConjugate}(p,q) \Rightarrow \operatorname{HolderConjugate}(q,p)$$$

Lean4

@[symm]
protected theorem symm : q.HolderConjugate p :=
  HolderTriple.symm h

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

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

Разделы

Аффилиация

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