instContMDiffVectorBundleOfSomeENatTopOfLEInfty

English

The zero section is C^n on any set t: ContMDiffOn holds for the zero section on t.

Русский

Нулевая секция гладкая на любом наборе t: ContMDiffOn для нулевой секции на t.

LaTeX

$$$\operatorname{ContMDiffOn} IB (IB. prod 𝓘(𝕜, F)) n (zeroSection F E) t$$$

Lean4

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

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