Theorems · Theorem · algebraic topology

ContinuousWithinAt.clm_apply_of_inCoordinates

∀ {𝕜 : Type u_8} {F₁ : Type u_9} {F₂ : Type u_10} {B₁ : Type u_11} {B₂ : Type u_12} {M : Type u_13}
  {E₁ : B₁ → Type u_14} {E₂ : B₂ → Type u_15} [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)]
  [inst_13 : TopologicalSpace B₁] [inst_14 : TopologicalSpace B₂] [inst_15 : TopologicalSpace M]
  [inst_16 : FiberBundle F₁ E₁] [inst_17 : VectorBundle 𝕜 F₁ E₁] [inst_18 : FiberBundle F₂ E₂]
  [inst_19 : VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)}
  {v : (m : M) → E₁ (b₁ m)} {s : Set M},
  ContinuousWithinAt (fun m => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s m₀ →
    ContinuousWithinAt (fun m => ⟨b₁ m, v m⟩) s m₀ →
      ContinuousWithinAt b₂ s m₀ → ContinuousWithinAt (fun m => ⟨b₂ m, (ϕ m) (v m)⟩) s m₀

Consider a continuous map v : M → E₁ to a vector bundle, over a base map b₁ : M → B₁, and another basemap b₂ : M → B₂. Given linear maps ϕ m : E₁ (b₁ m) → E₂ (b₂ m) depending continuously on m, one can apply ϕ m to g m, and the resulting map is continuous. Note that the continuity of ϕ cannot be always be stated as continuity of a map into a bundle, as the pullback bundles b₁ *ᵖ E₁ and b₂ *ᵖ E₂ only have a nice topology when b₁ and b₂ are globally continuous, but we want to apply this lemma with only local information. Therefore, we formulate it using continuity of ϕ read in coordinates. Version for ContinuousWithinAt. We also give a version for ContinuousAt, but no version for ContinuousOn or Continuous as our assumption, written in coordinates, only makes sense around a point. For a version with B₁ = B₂ and b₁ = b₂, in which continuity can be expressed without inCoordinates, see ContinuousWithinAt.clm_bundle_apply

Defined in

Mathlib.Topology.VectorBundle.Hom

Cited by

2 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommGroupModuleNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceAddCommGroupModuleNormedAddCommGroupNormedSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceTopologicalSpaceFiberBundleVectorBundleFiberBundleVectorBundle