instIsManifoldOfNatWithTopENatOfMinSmoothness

English

Compatibility of manifold-level statements with lower-order assumptions via instance transfer.

Русский

Совместимость утверждений на уровне многообразия с более низкими предпосылками через перенос экземпляров.

LaTeX

$$$\text{IsManifold} \ I (minSmoothness 𝕜 2) M \\rightarrow \text{IsManifold} \ I (minSmoothness 𝕜 1) M$$$

Lean4

instance {n : ℕ} [n.AtLeastTwo] [IsManifold I (minSmoothness 𝕜 (ofNat(n))) M] : IsManifold I (ofNat(n)) M :=
  IsManifold.of_le (n := minSmoothness 𝕜 n) le_minSmoothness

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