English
Let α be a type with the discrete topology and β a topological space. Then the continuous maps from α to β are in bijection with all functions from α to β; the correspondence is given by identifying a continuous map with its underlying function.
Русский
Пусть α имеет дискретную топологию, а β — топологическое пространство. Тогда непрерывные отображения α → β эквивалентны всем функциям α → β; соответствие даётся идентификацией непрерывного отображения с его базовой функцией.
LaTeX
$$$C(\alpha, \beta) \simeq (\alpha \to \beta)$$$
Lean4
/-- The continuous functions from `α` to `β` are the same as the plain functions when `α` is discrete.
-/
@[simps]
def equivFnOfDiscrete : C(α, β) ≃ (α → β) :=
⟨fun f => f, fun f => ⟨f, continuous_of_discreteTopology⟩, fun _ => by ext; rfl, fun _ => by ext; rfl⟩
