instContMDiffInv₀OfNatWithTopENat

Mathlib.Geometry.Manifold.Algebra.LieGroup

URI: https://scilib.ai/kg/mathlib#instContMDiffInv₀OfNatWithTopENat

English

Instance gives ContMDiffInv₀ at level 1 from level 2 for Nat/Top ENat.

Русский

Инстанс даёт ContMDiffInv₀ на уровне 1 из уровня 2 для Nat/Top ENat.

LaTeX

$$ContMDiffInv₀ I 1 G$$

Lean4

instance [ContMDiffInv₀ I 2 G] : ContMDiffInv₀ I 1 G :=
  ContMDiffInv₀.of_le one_le_two

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru