inner_bundle — Mathlib

English

The pointwise inner product of two E-valued maps is continuous at a point x.

Русский

По точке x скалярное произведение двух карт векторных пространств непрерывно.

LaTeX

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

Lean4

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

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