English
There is an equivalence of continuity statements for a total-space map and its coordinates under the hom-bundle framework.
Русский
Существуют эквивалентности непрерывности для отображения в полном пространстве и координат под структурой гом-бандла.
LaTeX
$$$\\text{Equiv}(\\text{ContinuousAt } f, (f.base, f.coord))$$$
Lean4
/-- Consider a continuous map `v : M → E₁` to a vector bundle, over a base map `b₁ : M → B₁`, and
another basemap `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending
continuously on `m`, one can apply `ϕ m` to `g m`, and the resulting map is continuous.
Note that the continuity of `ϕ` cannot be always be stated as continuity of a map into a bundle,
as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` only have a nice topology when `b₁` and `b₂` are
globally continuous, but we want to apply this lemma with only local information. Therefore, we
formulate it using continuity of `ϕ` read in coordinates.
Version for `ContinuousAt`. We also give a version for `ContinuousWithinAt`, but no version for
`ContinuousOn` or `Continuous` as our assumption, written in coordinates, only makes sense around
a point.
For a version with `B₁ = B₂` and `b₁ = b₂`, in which continuity can be expressed without
`inCoordinates`, see `ContinuousWithinAt.clm_bundle_apply`
-/
theorem clm_apply_of_inCoordinates
(hϕ : ContinuousAt (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀)
(hv : ContinuousAt (fun m ↦ (v m : TotalSpace F₁ E₁)) m₀) (hb₂ : ContinuousAt b₂ m₀) :
ContinuousAt (fun m ↦ (ϕ m (v m) : TotalSpace F₂ E₂)) m₀ :=
by
rw [← continuousWithinAt_univ] at hϕ hv hb₂ ⊢
exact hϕ.clm_apply_of_inCoordinates hv hb₂
