dense — Mathlib

English

The set of Lp-simple functions is dense in Lp(E,p,μ); i.e., the closure of Lp.simpleFunc inside Lp is all of Lp.

Русский

Множество Lp-поразностей простых функций плотно в Lp(E,p,μ); замыкание Lp.simpleFunc внутри Lp покрывает всю Lp.

LaTeX

$$$\overline{Lp.simpleFunc\, E\, p\, μ} = Lp\, E\, p\, μ$$$

Lean4

protected theorem dense (hp_ne_top : p ≠ ∞) : Dense (Lp.simpleFunc E p μ : Set (Lp E p μ)) := by
  simpa only [denseRange_subtype_val] using simpleFunc.denseRange (E := E) (μ := μ) hp_ne_top

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