instIsContinuousRiemannianBundleTrivial

English

A trivial bundle with an inner product on the fiber is a continuous Riemannian bundle.

Русский

Тривиальное расслоение с скалярным произведением на волокне является непрерывным риммановым расслоением.

LaTeX

$$$\\text{instance: IsContinuousRiemannianBundle } F_1 (Bundle.Trivial B F_1)$$$

Lean4

/-- A trivial vector bundle, in which the model fiber has a inner product,
is a Riemannian bundle. -/
instance : IsContinuousRiemannianBundle F₁ (Bundle.Trivial B F₁) :=
  by
  refine ⟨fun x ↦ innerSL ℝ, ?_, fun x v w ↦ rfl⟩
  rw [continuous_iff_continuousAt]
  intro x
  rw [FiberBundle.continuousAt_totalSpace]
  refine ⟨continuousAt_id, ?_⟩
  convert continuousAt_const (y := innerSL ℝ)
  ext v w
  simp [hom_trivializationAt_apply, inCoordinates, Trivialization.linearMapAt_apply]

Похожие утверждения