instIsContMDiffRiemannianBundleOfTopWithTopENat

English

A natural-number level via ENat-based lifting gives contMDiffRiemannianBundle at 0 or 1 based on base top.

Русский

Уровень натурального числа через ENat позволяет получить contMDiffRiemannianBundle на нуле или единице.

LaTeX

$$$IsContMDiffRiemannianBundle IB 0 F E \\Rightarrow IsContMDiffRiemannianBundle IB 1 F E$$$

Lean4

instance {a : WithTop ℕ∞} [IsContMDiffRiemannianBundle IB ω F E] : IsContMDiffRiemannianBundle IB a F E :=
  IsContMDiffRiemannianBundle.of_le le_top

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