Theorems · Theorem · global analysis

MDifferentiableWithinAt.clm_apply_of_inCoordinates

∀ {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {E₁ : B₁ → Type u_7}
  {E₂ : B₂ → Type u_8} [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B₁) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B₁) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B₁) → TopologicalSpace (E₁ x)]
  [inst_7 : (x : B₂) → AddCommGroup (E₂ x)] [inst_8 : (x : B₂) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_9} [inst_13 : NormedAddCommGroup EB₁]
  [inst_14 : NormedSpace 𝕜 EB₁] {HB₁ : Type u_10} [inst_15 : TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁}
  [inst_16 : TopologicalSpace B₁] [inst_17 : ChartedSpace HB₁ B₁] {EB₂ : Type u_11} [inst_18 : NormedAddCommGroup EB₂]
  [inst_19 : NormedSpace 𝕜 EB₂] {HB₂ : Type u_12} [inst_20 : TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂}
  [inst_21 : TopologicalSpace B₂] [inst_22 : ChartedSpace HB₂ B₂] {EM : Type u_13} [inst_23 : NormedAddCommGroup EM]
  [inst_24 : NormedSpace 𝕜 EM] {HM : Type u_14} [inst_25 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  [inst_26 : TopologicalSpace M] [inst_27 : ChartedSpace HM M] [inst_28 : FiberBundle F₁ E₁]
  [inst_29 : VectorBundle 𝕜 F₁ E₁] [inst_30 : FiberBundle F₂ E₂] [inst_31 : VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁}
  {b₂ : M → B₂}, ⋯

Consider a differentiable map v : M → E₁ to a vector bundle, over a basemap b₁ : M → B₁, and another basemap b₂ : M → B₂. Given linear maps ϕ m : E₁ (b₁ m) → E₂ (b₂ m) depending differentiably on m, one can apply ϕ m to g m, and the resulting map is differentiable. Note that the differentiability of ϕ cannot be always be stated as differentiability of a map into a manifold, as the pullback bundles b₁ *ᵖ E₁ and b₂ *ᵖ E₂ only make sense when b₁ and b₂ are globally smooth, but we want to apply this lemma with only local information. Therefore, we formulate it using differentiability of ϕ read in coordinates. Version for MDifferentiableWithinAt. We also give a version for MDifferentiableAt, but no version for MDifferentiableOn or MDifferentiable as our assumption, written in coordinates, only makes sense around a point.

Defined in

Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable

Cited by

3 results in Mathlib

Foundations

Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldAddCommGroupModuleNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceAddCommGroupModuleNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceChartedSpaceFiberBundleVectorBundleFiberBundleVectorBundle