unique

Mathlib.Data.ENNReal.Holder

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

English

Fix p,q; if r and r' both complete the HolderTriple with p,q, then r = r'.

Русский

Зафиксируем p,q; если r и r' образуют с ними HolderTriple, то r = r'.

LaTeX

$$∀ r' [hr' : HolderTriple p q r'], r = r'$$

Lean4

theorem unique (r' : ℝ≥0∞) [hr' : HolderTriple p q r'] : r = r' := by rw [← inv_inj, inv_eq p q r, inv_eq p q r']

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

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

Разделы

Аффилиация

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