contMDiffOn_section_baseSet_iff — Mathlib

English

The total space of a C^n vector bundle carries a C^n-differentiable structure when the base and fibers are set up with a compatible contMDiff vector bundle structure.

Русский

Общее пространство обладает структурой C^n.

LaTeX

$$$$\\text{ContMDiffOn }(\\text{TotalSpace }F E)\\; n \\;$$$$

Lean4

/-- For any trivialization `e`, the smoothness of a `C^n` section on `e.baseSet`
can be determined using `e`. -/
theorem contMDiffOn_section_baseSet_iff {s : ∀ x, E x}
    (e : Trivialization F (Bundle.TotalSpace.proj : Bundle.TotalSpace F E → B)) [MemTrivializationAtlas e] :
    ContMDiffOn IB (IB.prod 𝓘(𝕜, F)) n (fun x ↦ TotalSpace.mk' F x (s x)) e.baseSet ↔
      ContMDiffOn IB 𝓘(𝕜, F) n (fun x ↦ (e ⟨x, s x⟩).2) e.baseSet :=
  e.contMDiffOn_section_iff e.open_baseSet subset_rfl

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