continuousAt_hom_bundle — Mathlib

English

The trivialization at a basepoint x0 is continuous with respect to the base and coordinates.

Русский

Тривиализация в базовой точке x0 непрерывна по основаниям и координатам.

LaTeX

$$$\\text{Theorem: } (\\operatorname{trivializationAt} (\\text{ContinuousLinearMap }\\sigma F_1 F_2) (\\cdot)) \\\\text{is continuous at } x_0.$$$

Lean4

theorem continuousAt_hom_bundle {M : Type*} [TopologicalSpace M]
    (f : M → TotalSpace (F₁ →SL[σ] F₂) (fun x ↦ E₁ x →SL[σ] E₂ x)) {x₀ : M} :
    ContinuousAt f x₀ ↔
      ContinuousAt (fun x ↦ (f x).1) x₀ ∧
        ContinuousAt (fun x ↦ inCoordinates F₁ E₁ F₂ E₂ (f x₀).1 (f x).1 (f x₀).1 (f x).1 (f x).2) x₀ :=
  FiberBundle.continuousAt_totalSpace ..

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