memLp_of_hasCompactSupport — Mathlib

English

A continuous function with compact support belongs to Lp for any finite p.

Русский

Непрерывная функция с компактной поддержкой принадлежит Lp при любом конечном p.

LaTeX

$$Continuous.memLp_of_hasCompactSupport (hf : Continuous f) (h'f : HasCompactSupport f) : MemLp f p μ$$

Lean4

/-- A continuous function with compact support is in L^p. -/
theorem _root_.Continuous.memLp_of_hasCompactSupport [OpensMeasurableSpace X] {f : X → E} (hf : Continuous f)
    (h'f : HasCompactSupport f) : MemLp f p μ :=
  by
  have := hf.memLp_top_of_hasCompactSupport h'f μ
  exact
    this.mono_exponent_of_measure_support_ne_top (fun x ↦ image_eq_zero_of_notMem_tsupport) (h'f.measure_lt_top.ne)
      le_top

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