inner_bundle — Mathlib

English

In a continuous Riemannian bundle, the pointwise inner product is continuous.

Русский

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

LaTeX

$$$\\text{ContinuousAt}.inner_bundle$$$

Lean4

/-- Given two continuous maps into the same fibers of a continuous Riemannian bundle,
their inner product is continuous. -/
theorem inner_bundle (hv : Continuous (fun m ↦ (v m : TotalSpace F E)))
    (hw : Continuous (fun m ↦ (w m : TotalSpace F E))) : Continuous (fun b ↦ ⟪v b, w b⟫) :=
  by
  simp only [continuous_iff_continuousAt] at hv hw ⊢
  exact fun x ↦ (hv x).inner_bundle (hw x)

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