English
If β is a topological group, then the set of continuous maps α → β forms a Subgroup of the group of all maps α → β under pointwise multiplication.
Русский
Если β — топологическая группа, то множество непрерывных отображений α → β образует подпалку в группе всех отображений α → β относительно точечного умножения.
LaTeX
$$$\{ f: \alpha \to \beta \mid \text{Continuous}(f)\} \le \text{(Group of all maps) } (\alpha \to \beta).$$$
Lean4
/-- The subgroup of continuous maps `α → β`. -/
@[to_additive /-- The `AddSubgroup` of continuous maps `α → β`. -/
]
def continuousSubgroup (α : Type*) (β : Type*) [TopologicalSpace α] [TopologicalSpace β] [Group β]
[IsTopologicalGroup β] : Subgroup (α → β) :=
{ continuousSubmonoid α β with inv_mem' := fun fc => Continuous.inv fc }
