chartedSpace_chartAt — Mathlib

English

The fst component of the inverse chart in the fibre chart gives the base coordinate via the trivialization.

Русский

Первая компонента обратной чарты в волокне возвращает базовую координату через тривиализацию.

LaTeX

$$$$ ((chartAt (ModelProd HB F) x).symm y).proj = (chartAt HB x.proj).symm y.1. $$$$

Lean4

theorem chartedSpace_chartAt (x : TotalSpace F E) :
    chartAt (ModelProd HB F) x =
      (trivializationAt F E x.proj).toOpenPartialHomeomorph ≫ₕ
        (chartAt HB x.proj).prod (OpenPartialHomeomorph.refl F) :=
  by
  dsimp only [chartAt_comp, prodChartedSpace_chartAt, FiberBundle.chartedSpace'_chartAt, chartAt_self_eq]
  rw [Trivialization.coe_coe, Trivialization.coe_fst' _ (mem_baseSet_trivializationAt F E x.proj)]

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