restrict

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

English

If f ∈ Lp(μ), then f ∈ Lp(μ|_s) for any subset s.

Русский

Если f ∈ Lp(μ), то f ∈ Lp(μ|_s) для произвольной подмножества s.

LaTeX

$$$\\text{MemLp}(f,p, μ) \\Rightarrow \\text{MemLp}(f,p, μ\\restriction s).$$$

Lean4

theorem restrict (s : Set α) {f : α → ε} (hf : MemLp f p μ) : MemLp f p (μ.restrict s) :=
  hf.mono_measure Measure.restrict_le_self

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

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

Разделы

Аффилиация

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