Theorems · Theorem · algebraic topology

eventually_norm_symmL_trivializationAt_comp_self_lt

∀ {B : Type u_1} [inst : TopologicalSpace B] (F : Type u_2) [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  (E : B → Type u_3) [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E]
  [h : IsContinuousRiemannianBundle F E] (x : B) {r : ℝ},
  1 < r →
    ∀ᶠ (y : B) in nhds x,
      ‖Bundle.Trivialization.symmL ℝ (trivializationAt F E x) y ∘SL
            Bundle.Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x‖ <
        r

In a continuous Riemannian bundle, local changes of coordinates given by the trivialization at a point distort the norm by a factor arbitrarily close to 1.

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupInnerProductSpaceFiberBundleVectorBundleIsContinuousRiemannianBundle