chartedSpace_chartAt_symm_fst — Mathlib

English

The symm of the total-space chart maps back to base chart coordinates in the fibre coordinate.

Русский

Симметрия обратной чарты отображает обратно базовые координаты в координате волокна.

LaTeX

$$$$ chartedSpace_chartAt_symm (x) (y) = \\dots $$$$

Lean4

theorem chartedSpace_chartAt_symm_fst (x : TotalSpace F E) (y : ModelProd HB F)
    (hy : y ∈ (chartAt (ModelProd HB F) x).target) :
    ((chartAt (ModelProd HB F) x).symm y).proj = (chartAt HB x.proj).symm y.1 :=
  by
  simp only [FiberBundle.chartedSpace_chartAt, mfld_simps] at hy ⊢
  exact (trivializationAt F E x.proj).proj_symm_apply hy.2

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