Theorems · Theorem · algebraic topology

eventually_norm_trivializationAt_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),
  ∃ C > 0, ∀ᶠ (y : B) in nhds x, ‖Bundle.Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) y‖ < C

In a continuous Riemannian bundle, the trivialization at a point is locally bounded in norm.

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceNormedAddCommGroupNormedSpaceTopologicalSpaceNormedAddCommGroupInnerProductSpaceFiberBundleVectorBundleIsContinuousRiemannianBundle