English
In a continuous Riemannian bundle, the inner product of two continuous bundle maps is continuous on 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 `ContinuousWithinAt`. -/
theorem inner_bundle (hv : ContinuousWithinAt (fun m ↦ (v m : TotalSpace F E)) s x)
(hw : ContinuousWithinAt (fun m ↦ (w m : TotalSpace F E)) s x) : ContinuousWithinAt (fun m ↦ ⟪v m, w m⟫) s x :=
by
rcases h.exists_continuous with ⟨g, g_cont, hg⟩
have hf : ContinuousWithinAt b s x :=
by
simp only [FiberBundle.continuousWithinAt_totalSpace] at hv
exact hv.1
simp only [hg]
have : ContinuousWithinAt (fun m ↦ TotalSpace.mk' ℝ (E := Bundle.Trivial B ℝ) (b m) (g (b m) (v m) (w m))) s x :=
(g_cont.continuousAt.comp_continuousWithinAt hf).clm_bundle_apply₂ (F₁ := F) (F₂ := F) hv hw
simp only [FiberBundle.continuousWithinAt_totalSpace] at this
exact this.2
