instOfNatWithTopENat_2 — Mathlib

English

If M has a C^3-manifold structure modeled by I, then M also has a C^2-manifold structure modeled by the same I.

Русский

Если у M есть структура C^3-многообразия, моделируемая по I, то M также является C^2-многообразием по той же модели.

LaTeX

$$IsManifold(I,3,M) \rightarrow IsManifold(I,2,M)$$

Lean4

instance [IsManifold I 3 M] : IsManifold I 2 M :=
  IsManifold.of_le (n := 3) (by norm_cast)

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