isHomeomorph_coe — Mathlib

English

The coercion map from the space of continuous maps C(X,Y) to the function space X→Y is a homeomorphism (i.e., it is a homeomorphism between these two function spaces).

Русский

Эмпирическое отображение из пространства непрерывных отображений C(X,Y) в пространство функций X→Y является гомеоморфизмом между этими двумя пространствами функций.

LaTeX

$$$\text{IsHomeomorph}((\cdot) : C(X,Y) \to X^Y)$$$

Lean4

theorem isHomeomorph_coe : IsHomeomorph ((⇑) : C(X, Y) → X → Y) :=
  homeoFnOfDiscrete.isHomeomorph

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