instIsManifoldOfNatWithTopENatOfMinSmoothness_1

English

Instances showing the manifold structure at various smoothness levels ensure well-defined Lie brackets.

Русский

Экземпляры дают множество структур многообразия на разных уровнях гладкости, обеспечивая определенность скобки Ли.

LaTeX

$$$\text{instIsManifoldMinSmoothnessOfNatWithTopENat}$$$

Lean4

instance [IsManifold I (minSmoothness 𝕜 1) M] : IsManifold I 1 M :=
  IsManifold.of_le (n := minSmoothness 𝕜 1) le_minSmoothness

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