isUniformEmbedding_coe — Mathlib

English

The embedding of Path x y into C(I, X) via the coordinatewise evaluation is an IsUniformEmbedding.

Русский

Встраивание Path x y в C(I, X) по координатному отображению является изометрным вложением.

LaTeX

$$$IsUniformEmbedding((\\uparrow): Path\,x\,y \\to C(I,X))$$$

Lean4

theorem isUniformEmbedding_coe : IsUniformEmbedding ((↑) : Path x y → C(I, X))
    where
  comap_uniformity := rfl
  injective := ContinuousMap.coe_injective'

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