unique

Mathlib.Data.ENNReal.Holder

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

English

For a fixed p, if q and q' both satisfy HolderConjugate p, then q = q'.

Русский

Для фиксированного p, если q и q' оба удовлетворяют HolderConjugate p, то q = q'.

LaTeX

$$HolderConjugate p q \\land \forall q' (HolderConjugate p q' \Rightarrow q = q')$$

Lean4

theorem unique (q' : ℝ≥0∞) [hq' : HolderConjugate p q'] : q = q' :=
  HolderTriple.unique_of_ne_zero p q q' one_ne_zero

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

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

Разделы

Аффилиация

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