isDenseEmbedding — Mathlib

English

The inclusion of Lp.simpleFunc into Lp E p μ is a densely embedded subspace.

Русский

Включение Lp.simpleFunc в Lp является плотным вложением.

LaTeX

$$$ \\text{IsDenseEmbedding}(\\iota) \\quad \\text{where } \\iota: Lp.simpleFunc E p μ \\hookrightarrow Lp E p μ$$$

Lean4

theorem isDenseEmbedding (hp_ne_top : p ≠ ∞) : IsDenseEmbedding ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
  by
  borelize E
  apply simpleFunc.isUniformEmbedding.isDenseEmbedding
  intro f
  rw [mem_closure_iff_seq_limit]
  have hfi' : MemLp f p μ := Lp.memLp f
  haveI : SeparableSpace (range f ∪ {0} : Set E) := (Lp.stronglyMeasurable f).separableSpace_range_union_singleton
  refine
    ⟨fun n =>
      toLp (SimpleFunc.approxOn f (Lp.stronglyMeasurable f).measurable (range f ∪ {0}) 0 _ n)
        (SimpleFunc.memLp_approxOn_range (Lp.stronglyMeasurable f).measurable hfi' n),
      fun n => mem_range_self _, ?_⟩
  convert SimpleFunc.tendsto_approxOn_range_Lp hp_ne_top (Lp.stronglyMeasurable f).measurable hfi'
  rw [toLp_coeFn f (Lp.memLp f)]

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