Theorems · Theorem · algebraic topology

Bundle.RiemannianMetric.continuousAt

∀ {B : Type u_4} {E : B → Type u_6} [inst : (b : B) → TopologicalSpace (E b)] [inst_1 : (b : B) → AddCommGroup (E b)]
  [inst_2 : (b : B) → Module ℝ (E b)] (self : Bundle.RiemannianMetric E) (b : B),
  ContinuousAt (fun v => ((self.inner b) v) v) 0

The continuity at 0 is automatic when E b is isomorphic to a normed space, but since we are not making this assumption here we have to include it.

Defined in

Mathlib.Topology.VectorBundle.Riemannian

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceAddCommGroupModule