coe_homeoFnOfDiscrete — Mathlib

English

The forward direction of the natural equivalence between C(X,Y) and X→Y is simply the identity on functions; i.e., the forward map sends a continuous map to the same function it represents.

Русский

Впереди естественного биекции между C(X,Y) и X→Y отображение отправляет непрерывное отображение в ту же самую функцию, которую оно представляет.

LaTeX

$$$(homeoFnOfDiscrete)_{\mathrm{toFun}}(f) = f \quad \forall f \in C(X,Y)$$$

Lean4

@[simp]
theorem coe_homeoFnOfDiscrete : ⇑homeoFnOfDiscrete = (DFunLike.coe : C(X, Y) → X → Y) :=
  rfl

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