toContinuousMap_injective — Mathlib

English

The forgetful map toContinuousMap: C(X,R)₀ → C(X,R) is injective; i.e., two basepoint-preserving maps are equal if they have the same underlying continuous map.

Русский

Отображение toContinuousMap: C(X,R)₀ → C(X,R) инъективно; то есть два отображения, сохраняющие ноль, равны, если их как обычные непрерывные отображения совпадают.

LaTeX

$$$\\text{toContinuousMap is injective}$$$

Lean4

theorem toContinuousMap_injective : Injective ((↑) : C(X, R)₀ → C(X, R)) := fun _ _ h ↦ congr(.mk $(h) _)

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