instLieGroupOfSomeENatTopOfLEInfty

English

If a Lie group structure exists for I at the ω-th level (∞), then for any a with a ≤ ∞ (i.e., any a in WithTop ENat) there is a Lie group structure for I on G at level a.

Русский

Если существует структура LieGroup для I на уровне ω (бесконечность), то для любого a ≤ ∞ существует структура LieGroup для I на уровне a.

LaTeX

$$$[LieGroup I (WithTop.some instTopENat.top) G] \land [h: ENat.LEInfty\ a] \Rightarrow [LieGroup I a G].$$$

Lean4

@[to_additive]
instance {a : WithTop ℕ∞} [LieGroup I ∞ G] [h : ENat.LEInfty a] : LieGroup I a G :=
  LieGroup.of_le h.out

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