coe_equivFnOfDiscrete — Mathlib

English

The forward part of the canonical equivalence between continuous maps α → β and functions α → β is just the underlying function map.

Русский

Прямое отображение канонического биективного соответствия между непрерывными отображениями α → β и функциями α → β есть просто сопоставление функции без учёта условия непрерывности.

LaTeX

$$$\operatorname{equivFnOfDiscrete}(f) = f \quad \text{as a function } (\alpha \to \beta)$$$

Lean4

@[simp]
theorem coe_equivFnOfDiscrete : ⇑equivFnOfDiscrete = (DFunLike.coe : C(α, β) → α → β) :=
  rfl

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