toContinuousMap_injective — Mathlib

English

The map toContinuousMap: LocallyConstant X Y → C(X, Y) is injective: if toContinuousMap f = toContinuousMap g, then f = g.

Русский

Отображение toContinuousMap: LocallyConstant(X,Y) → C(X,Y) инъективно: если toContinuousMap(f) = toContinuousMap(g), тогда f = g.

LaTeX

$$$\\\\forall f,g:\\\\mathrm{LocallyConstant}(X,Y), \\\\mathrm{toContinuousMap}(f) = \\\\mathrm{toContinuousMap}(g) \\\\Rightarrow f=g$$$

Lean4

theorem toContinuousMap_injective : Function.Injective (toContinuousMap : LocallyConstant X Y → C(X, Y)) := fun _ _ h =>
  ext (ContinuousMap.congr_fun h)

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