trivializationAt_model_space_apply

English

The symmL of the trivialization at b is the identity on model-space-coordinates, i.e., equals 1.

Русский

СиммL тривиализации равен тождественному отображению в координатах модельного пространства.

LaTeX

$$$(\mathrm{trivializationAt}\;E\,(\mathrm{TangentSpace}\,I)\;b).\mathrm{symmL} 𝕜 b = 1$$$

Lean4

@[simp, mfld_simps]
theorem trivializationAt_model_space_apply (p : TangentBundle I H) (x : H) :
    trivializationAt E (TangentSpace I) x p = (p.1, p.2) :=
  by
  simp only [TangentBundle.trivializationAt_apply]
  have : fderivWithin 𝕜 (↑I ∘ ↑I.symm) (range I) (I p.proj) = fderivWithin 𝕜 id (range I) (I p.proj) :=
    fderivWithin_congr' (fun y hy ↦ by simp [hy]) (mem_range_self p.proj)
  simp [this, fderivWithin_id (ModelWithCorners.uniqueDiffWithinAt_image I)]

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