mk_contMDiffCoordChange — Mathlib

English

The contMDiffCoordChange map agrees with the explicit fiberwise coordinate formula when evaluated at a base point b in the intersection and fiber value v.

Русский

Сходимость и согласованность координатного перехода.

LaTeX

$$$$\\forall b\\in e.baseSet\\cap e'.baseSet, \\; contMDiffCoordChange(n,IB,e, e', b)\\, v = e'⟨ b, e.symm b v ⟩.2.$$$$

Lean4

theorem mk_contMDiffCoordChange (he : e ∈ a.pretrivializationAtlas) (he' : e' ∈ a.pretrivializationAtlas) {b : B}
    (hb : b ∈ e.baseSet ∩ e'.baseSet) (v : F) : (b, a.contMDiffCoordChange n IB he he' b v) = e' ⟨b, e.symm b v⟩ :=
  by
  ext
  · rw [e.mk_symm hb.1 v, e'.coe_fst', e.proj_symm_apply' hb.1]
    rw [e.proj_symm_apply' hb.1]; exact hb.2
  · exact a.contMDiffCoordChange_apply he he' hb v

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