chartedSpace — Mathlib

English

The chart at a total space point is given by the trivialization symmetry with the base chart, and it respects the projection coordinates.

Русский

Чарт при точке пространства-total выражается тривилизацией симметрии и сохраняет координаты проекции.

LaTeX

$$$$ chartAt^{ModelProd HB F}_x = trivializationAt F E x.proj \\circ (chartAt HB x.proj) \\times (OpenPartialHomeomorph.refl F). $$$$

Lean4

/-- Let `B` be a charted space modelled on `HB`.  Then a fiber bundle `E` over a base `B` with model
fiber `F` is naturally a charted space modelled on `HB.prod F`. -/
instance chartedSpace : ChartedSpace (ModelProd HB F) (TotalSpace F E) :=
  ChartedSpace.comp _ (B × F) _

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