Theorems · Theorem · algebraic topology

VectorBundleCore.inCoordinates_eq

∀ {B : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : TopologicalSpace B] {𝕜₁ : Type u_5}
  {𝕜₂ : Type u_6} [inst_2 : NontriviallyNormedField 𝕜₁] [inst_3 : NontriviallyNormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂}
  {B' : Type u_7} [inst_4 : TopologicalSpace B'] [inst_5 : NormedSpace 𝕜₁ F] {F' : Type u_8}
  [inst_6 : NormedAddCommGroup F'] [inst_7 : NormedSpace 𝕜₂ F'] {ι : Type u_10} {ι' : Type u_11}
  (Z : VectorBundleCore 𝕜₁ B F ι) (Z' : VectorBundleCore 𝕜₂ B' F' ι') {x₀ x : B} {y₀ y : B'} (ϕ : F →SL[σ] F'),
  x ∈ Z.baseSet (Z.indexAt x₀) →
    y ∈ Z'.baseSet (Z'.indexAt y₀) →
      ContinuousLinearMap.inCoordinates F Z.Fiber F' Z'.Fiber x₀ x y₀ y ϕ =
        Z'.coordChange (Z'.indexAt y) (Z'.indexAt y₀) y ∘SL ϕ ∘SL Z.coordChange (Z.indexAt x₀) (Z.indexAt x) x

Rewrite ContinuousLinearMap.inCoordinates in a VectorBundleCore.

Defined in

Mathlib.Topology.VectorBundle.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupTopologicalSpaceNontriviallyNormedFieldNontriviallyNormedFieldTopologicalSpaceNormedSpaceNormedAddCommGroupNormedSpace