instContMDiffVectorBundleOfNatWithTopENat_1

English

The symmetrized fibre coordinate change map is ContMDiffOn, i.e., differentiable on the intersection of the base sets.

Русский

Симметризированное отображение смены координат гладко на пересечении базовых множеств.

LaTeX

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

Lean4

instance : ContMDiffVectorBundle 0 F E IB := by
  constructor
  intro e e' he he'
  rw [contMDiffOn_zero_iff]
  exact VectorBundle.continuousOn_coordChange' e e'

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