English
The set of continuous maps α → β forms a Submonoid of the full function space α → β, closed under pointwise multiplication and containing the constant 1 map.
Русский
Множество непрерывных отображений α → β образует подмоноид на всем пространстве функций α → β, замкнутое относительно покомножения и содержащее константное 1.
LaTeX
$$$\{ f:\alpha \to \beta \mid \text{Continuous}(f)\} \text{ является подмоноидом } (\alpha \to \beta) \text{ с точечным умножением}.$$$
Lean4
/-- The `Submonoid` of continuous maps `α → β`. -/
@[to_additive /-- The `AddSubmonoid` of continuous maps `α → β`. -/
]
def continuousSubmonoid (α : Type*) (β : Type*) [TopologicalSpace α] [TopologicalSpace β] [MulOneClass β]
[ContinuousMul β] : Submonoid (α → β)
where
carrier := {f : α → β | Continuous f}
one_mem' := @continuous_const _ _ _ _ 1
mul_mem' fc gc := fc.mul gc
