one_le

Mathlib.Data.ENNReal.Holder

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

English

If p and q are HolderConjugate, then 1 ≤ p.

Русский

Если p и q удовлетворяют HolderConjugate, то 1 ≤ p.

LaTeX

$$HolderConjugate p q \Rightarrow 1 \le p$$

Lean4

theorem one_le : 1 ≤ p :=
  HolderTriple.le p q 1

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

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

Разделы

Аффилиация

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