inner_bundle — Mathlib

English

The inner product of two bundle-valued maps is continuous within a set.

Русский

Внутреннее произведение отображений в пакетах непрерывно внутри множества.

LaTeX

$$$\\text{ContinuousWithinAt}.inner_bundle$$$

Lean4

/-- Given two continuous maps into the same fibers of a continuous Riemannian bundle,
their inner product is continuous. Version with `ContinuousOn`. -/
theorem inner_bundle (hv : ContinuousOn (fun m ↦ (v m : TotalSpace F E)) s)
    (hw : ContinuousOn (fun m ↦ (w m : TotalSpace F E)) s) : ContinuousOn (fun b ↦ ⟪v b, w b⟫) s := fun x hx ↦
  (hv x hx).inner_bundle (hw x hx)

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