LpAddConst_of_one_le

Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

URI: https://scilib.ai/kg/mathlib#MeasureTheory.LpAddConst_of_one_le

← MathLib Explorer

English

LpAddConst(p) < ∞ for all p.

Русский

LpAddConst(p) < ∞ для любого p.

LaTeX

$$$\\operatorname{LpAddConst}(p) < \\infty$$$

Lean4

theorem LpAddConst_of_one_le {p : ℝ≥0∞} (hp : 1 ≤ p) : LpAddConst p = 1 :=
  by
  rw [LpAddConst, if_neg]
  intro h
  exact lt_irrefl _ (h.2.trans_le hp)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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