isContMDiff — Mathlib

English

The vector prebundle of continuous linear maps is shown to be ContMDiff under the given coordinate conditions.

Русский

Векторное предрасслоение непрерывно линейных отображений гладко по заданным условиям координат.

LaTeX

$$$\\text{vectorPrebundle}$ IsContMDiff$$

Lean4

instance isContMDiff : (Bundle.ContinuousLinearMap.vectorPrebundle (RingHom.id 𝕜) F₁ E₁ F₂ E₂).IsContMDiff IB n where
  exists_contMDiffCoordChange :=
    by
    rintro _ ⟨e₁, e₂, he₁, he₂, rfl⟩ _ ⟨e₁', e₂', he₁', he₂', rfl⟩
    exact
      ⟨continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂', contMDiffOn_continuousLinearMapCoordChange,
        continuousLinearMapCoordChange_apply (RingHom.id 𝕜) e₁ e₁' e₂ e₂'⟩

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