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