boundedContinuousFunction_topologicalClosure

English

For integrable f, there exists g with compact support, such that ∫ ‖f−g‖ ≤ ε and g is integrable and bounded-continuous.

Русский

Для интегрируемой f существует g с компактной опорой, такая что ∫ ‖f−g‖ ≤ ε и g интегрируема и ограниченно непрерывна.

LaTeX

$$$\\exists g : α \\to E, HasCompactSupport g ∧ (∫ x, ‖f x - g x‖ ∂μ) ≤ ε ∧ Continuous g ∧ Integrable g μ$$$

Lean4

/-- A function in `Lp` can be approximated in `Lp` by continuous functions. -/
theorem boundedContinuousFunction_topologicalClosure [SecondCountableTopologyEither α E] [Fact (1 ≤ p)] (hp : p ≠ ∞)
    [μ.WeaklyRegular] : (boundedContinuousFunction E p μ).topologicalClosure = ⊤ :=
  SetLike.ext' <| (boundedContinuousFunction_dense E μ hp).closure_eq

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