isUniformInducing — Mathlib

English

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

Русский

Включение Lp.simpleFunc в Lp является равномерно-индуктивным отображением.

LaTeX

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

Lean4

theorem isUniformInducing : IsUniformInducing ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
  simpleFunc.isUniformEmbedding.isUniformInducing

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