isUniformEmbedding — Mathlib

English

The natural embedding of simple Lp functions into Lp is a uniform embedding; it is an injective map that preserves uniform structure.

Русский

Естественная вложение простых функций Lp в Lp является равномерной вложенностью; это внедрение с сохранением равномерной структуры.

LaTeX

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

Lean4

theorem isUniformEmbedding : IsUniformEmbedding ((↑) : Lp.simpleFunc E p μ → Lp E p μ) :=
  isUniformEmbedding_comap Subtype.val_injective

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