instIsContMDiffRiemannianBundleOfSomeENatTopOfLEInfty

English

An ENat-based lifting of contMDiffRiemannianBundle is downward closed with respect to LEInfty order.

Русский

Разновидность ENat для contMDiffRiemannianBundle сохраняет свойство при спуске по порядку LEInfty.

LaTeX

$$$\\forall a, b \\in WithTop\\, ENat,\\; a \\le b \\Rightarrow IsContMDiffRiemannianBundle IB b F E \\Rightarrow IsContMDiffRiemannianBundle IB a F E$$$

Lean4

instance {a : WithTop ℕ∞} [IsContMDiffRiemannianBundle IB ∞ F E] [h : LEInfty a] :
    IsContMDiffRiemannianBundle IB a F E :=
  IsContMDiffRiemannianBundle.of_le h.out

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