instContMDiffVectorBundleOfTopWithTopENat

English

The collection of fibre coordinate change maps is ContMDiffOn, given two trivializations e and e'.

Русский

Набор отображений смены координат волокна гладок на множестве, заданном тривиализациями e и e'.

LaTeX

$$$\operatorname{contMDiffOn_coordChangeL} e e' :\; \dots$$$

Lean4

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

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