semigroup — Mathlib

English

If G is a semigroup with a topology and charted space structure, then the set of C^n-maps from N to G forms a semigroup under pointwise multiplication.

Русский

Если G — полугруппа с топологией и структурой локальной картизации, то множество C^n-отображений из N в G образует полугруппу при точечном произведении.

LaTeX

$$$\text{If }(G,\cdot)\text{ is a topological semigroup with charted space, then }C^n\langle I,N;I',G\rangle\text{ is a semigroup with }(f\cdot g)(x)=f(x)\cdot g(x).$$$

Lean4

@[to_additive]
instance semigroup {G : Type*} [Semigroup G] [TopologicalSpace G] [ChartedSpace H' G] [ContMDiffMul I' n G] :
    Semigroup C^n⟮I, N; I', G⟯ :=
  DFunLike.coe_injective.semigroup _ coe_mul

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