instNormedSpaceLieAddGroup — Mathlib

English

There is a LieAddGroup structure on the model with corners 𝓘(𝕜,E) induced by the negation map being C^1 (or smoother).

Русский

На модели с углами 𝓘(𝕜,E) существует структура LieAddGroup, заданная гладкостью отрицания.

LaTeX

$$LieAddGroup 𝓘(𝕜, E) n E with contMDiff_neg = contDiff_neg.contMDiff$$

Lean4

instance instNormedSpaceLieAddGroup {𝕜 : Type*} [NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type*}
    [NormedAddCommGroup E] [NormedSpace 𝕜 E] : LieAddGroup 𝓘(𝕜, E) n E where contMDiff_neg := contDiff_neg.contMDiff

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