eLpNorm_le_add_measure_right

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

← MathLib Explorer

English

If MemLp f on μ+ν, then f is MemLp on μ.

Русский

Если MemLp f на μ+ν, то f ∈ MemLp на μ.

LaTeX

$$MemLp f p (μ+ν) → MemLp f p μ.$$

Lean4

theorem eLpNorm_le_add_measure_right (f : α → ε) (μ ν : Measure α) {p : ℝ≥0∞} : eLpNorm f p μ ≤ eLpNorm f p (μ + ν) :=
  eLpNorm_mono_measure f <| Measure.le_add_right <| le_refl _

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

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

Разделы

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

Аффилиация

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