mem_lpMeas_indicatorConstLp — Mathlib

English

For a measurable set s with finite measure, the indicator-constrained constant function belongs to lpMeas.

Русский

Для измеримой множества s с конечной мерой индикаторная константная функция принадлежит lpMeas.

LaTeX

$$$\text{indicatorConstLp}(p, m, μ, s, hμs, c) \in \ lpMeas(F, p, μ)$$$

Lean4

theorem mem_lpMeas_indicatorConstLp {m m0 : MeasurableSpace α} (hm : m ≤ m0) {μ : Measure α} {s : Set α}
    (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) {c : F} : indicatorConstLp p (hm s hs) hμs c ∈ lpMeas F 𝕜 m p μ :=
  ⟨s.indicator fun _ : α => c, (@stronglyMeasurable_const _ _ m _ _).indicator hs, indicatorConstLp_coeFn⟩

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