measure_support_lt_top_of_memLp — Mathlib

English

If MemLp holds, then the preimage of nonzero y has finite measure; generalization of the previous result.

Русский

Если MemLp выполняется, то прообраз не нулевого значения имеет конечную меру.

LaTeX

$$$\\mathrm{MemLp}(f,p,\\mu) \\Rightarrow \\forall y\\,(y\\neq 0\\Rightarrow \\mu(f^{-1}(\\{y\\}))<\\infty)$$$

Lean4

theorem measure_support_lt_top_of_memLp (f : α →ₛ E) (hf : MemLp f p μ) (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    μ (support f) < ∞ :=
  f.measure_support_lt_top ((memLp_iff hp_ne_zero hp_ne_top).mp hf)

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