instAddMonoidWithOneOfContinuousAdd

English

If α is a space and β is an AddMonoidWithOne with ContinuousAdd, then C(α, β) is an AddMonoidWithOne under pointwise operations.

Русский

Если α — пространство, β — AddMonoidWithOne с ContinuousAdd, то C(α, β) является AddMonoidWithOne по точечному умножению.

LaTeX

$$$\text{AddMonoidWithOne}(C(α,β))$$$

Lean4

instance {α : Type*} {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [AddMonoidWithOne β] [ContinuousAdd β] :
    AddMonoidWithOne C(α, β) :=
  coe_injective.addMonoidWithOne _ coe_zero coe_one coe_add coe_nsmul coe_natCast

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