instTopologicalSpace — Mathlib

English

The natural map toContinuousMap: ContinuousMonoidHom A B → C(A,B) is inducing; i.e., the topology on ContinuousMonoidHom A B is the pullback of the compact-open topology via toContinuousMap.

Русский

Естественное отображение toContinuousMap: ContinuousMonoidHom A B → C(A,B) индуцирует топологию; то есть топология на ContinuousMonoidHom A B получается как обратное изображение компактно-открытой топологии через toContinuousMap.

LaTeX

$$$\operatorname{IsInducing}\bigl(\mathrm{toContinuousMap} : \mathrm{ContinuousMonoidHom}\,A\,B \to C(A,B)\bigr).$$$

Lean4

@[to_additive]
instance : TopologicalSpace (ContinuousMonoidHom A B) :=
  TopologicalSpace.induced toContinuousMap ContinuousMap.compactOpen

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