denseRange — Mathlib

English

Let p be finite (1 ≤ p). Then the natural inclusion of the space of Lp-simple functions into the Lp space is dense; i.e., every Lp function can be approximated in the Lp-norm by simple Lp-functions.

Русский

Пусть p конечен и выполняется 1 ≤ p. Тогда естественное вложение пространства простых функций в Lp-п пространство плотно: любую функцию в Lp можно аппроксимировать в норме Lp простыми функциями.

LaTeX

$$$\operatorname{DenseRange}\big((\uparrow) : \! Lp.simpleFunc\, E\, p\, μ \to Lp\, E\, p\, μ\big)$$$

Lean4

protected theorem denseRange (hp_ne_top : p ≠ ∞) : DenseRange ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
  (simpleFunc.isDenseInducing hp_ne_top).dense

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