lt_top_iff_one_lt

Mathlib.Data.ENNReal.Holder

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

English

For HolderConjugate p q, p < ∞ iff 1 < q.

Русский

Для HolderConjugate p q: p < ∞ тогда и только тогда, когда 1 < q.

LaTeX

$$p < \infty \iff 1 < q$$

Lean4

theorem lt_top_iff_one_lt : p < ∞ ↔ 1 < q :=
  by
  rw [lt_top_iff_ne_top, ne_top_iff_ne_one _ q, ne_comm, lt_iff_le_and_ne]
  simp [one_le q p]

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

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

Разделы

Аффилиация

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