English
Let X be a space with a distinguished point 0 and R a topological additive group. Then the set of all continuous maps X → R that vanish at 0, denoted C(X, R)₀, carries the structure of a commutative Addison group under pointwise addition; in particular, (C(X, R)₀, +, 0) is a commutative group.
Русский
Пусть X — пространство с фиксированной точкой 0 и R — топологическая аддитивная группа. Тогда множество непрерывных отображений X → R, которые обращаются в 0 в точке 0, образуют аддитивную коммутативную группу под точечной операцией сложения; то есть (C(X, R)₀, +, 0) является коммутативной группой.
LaTeX
$$$\\text{AddCommGroup} (\\text{ContinuousMapZero } X\\ R)$$$
Lean4
instance instAddCommGroup : AddCommGroup C(X, R)₀ :=
fast_instance%toContinuousMap_injective.addCommGroup _ rfl (fun _ _ ↦ rfl) (fun _ ↦ rfl) (fun _ _ ↦ rfl)
(fun _ _ ↦ rfl) (fun _ _ ↦ rfl)
