instLieGroupOfTopWithTopENat — Mathlib

English

If there is a Lie group structure at the ω-top level, then for any a ≤ top there is a Lie group structure at level a.

Русский

Если существует структура LieGroup на уровне ω-сверху, то для любого a ≤ top существует структура LieGroup на уровне a.

LaTeX

$$[LieGroup I a G] given [LieGroup I WithTop.top.top G].$$

Lean4

@[to_additive]
instance {a : WithTop ℕ∞} [LieGroup I ω G] : LieGroup I a G :=
  LieGroup.of_le le_top

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