of_le — Mathlib

English

If a Lie group structure exists at a larger index n, then a Lie group structure also exists at any smaller index m ≤ n.

Русский

Если существует структура LieGroup при большем индексе n, то такая структура существует и при меньшем индексе m ≤ n.

LaTeX

$$$m,n : WithTop\ ENat\, m \le n \;\Rightarrow\; [\text{LieGroup } I n G] \Rightarrow [\text{LieGroup } I m G].$$$

Lean4

@[to_additive]
protected theorem of_le {m n : WithTop ℕ∞} (hmn : m ≤ n) [h : LieGroup I n G] : LieGroup I m G :=
  by
  have : ContMDiffMul I m G := ContMDiffMul.of_le hmn
  exact ⟨h.contMDiff_inv.of_le hmn⟩

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