English
If β is a group and IsTopologicalGroup β, then C(α, β) carries a group structure with pointwise multiplication and inversion.
Русский
Если β — группа и IsTopologicalGroup β, то C(α, β) наделяется групповой структурой по точечному умножению и инверсии.
LaTeX
$$$C(\alpha, \beta)$ is a group under pointwise operations when $β$ is a topological group$$
Lean4
@[to_additive]
instance [CommGroup β] [IsTopologicalGroup β] : IsTopologicalGroup C(α, β)
where
continuous_mul := by
letI : UniformSpace β := IsTopologicalGroup.toUniformSpace β
have : IsUniformGroup β := isUniformGroup_of_commGroup
rw [continuous_iff_continuousAt]
rintro ⟨f, g⟩
rw [ContinuousAt, tendsto_iff_forall_isCompact_tendstoUniformlyOn, nhds_prod_eq]
exact fun K hK =>
uniformContinuous_mul.comp_tendstoUniformlyOn
((tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK).prodMk
(tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK))
continuous_inv := by
letI : UniformSpace β := IsTopologicalGroup.toUniformSpace β
have : IsUniformGroup β := isUniformGroup_of_commGroup
rw [continuous_iff_continuousAt]
intro f
rw [ContinuousAt, tendsto_iff_forall_isCompact_tendstoUniformlyOn]
exact fun K hK =>
uniformContinuous_inv.comp_tendstoUniformlyOn
(tendsto_iff_forall_isCompact_tendstoUniformlyOn.mp Filter.tendsto_id K hK)
