mono_measure

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.MemLp.mono_measure

← MathLib Explorer

English

If ν ≤ μ then MemLp f p μ implies MemLp f p ν.

Русский

Если ν ≤ μ, то принадлежность к L^p по μ влечет принадлежность к L^p по ν.

LaTeX

$$$\nu \le μ \rightarrow (\text{MemLp}(f,p,μ) \rightarrow \text{MemLp}(f,p,ν))$$$

Lean4

theorem mono_measure {f : α → ε} (hμν : ν ≤ μ) (hf : MemLp f p μ) : MemLp f p ν :=
  ⟨hf.1.mono_measure hμν, (eLpNorm_mono_measure f hμν).trans_lt hf.2⟩

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

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

Разделы

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

Аффилиация

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