isDenseInducing — Mathlib

English

The inclusion map from Lp.simpleFunc to Lp is a dense inducing map.

Русский

Включение Lp.simpleFunc в Lp является плотной индукцией.

LaTeX

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

Lean4

protected theorem isDenseInducing (hp_ne_top : p ≠ ∞) : IsDenseInducing ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
  (simpleFunc.isDenseEmbedding hp_ne_top).isDenseInducing

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