tangentMap_comp_at — Mathlib

English

For a tangent bundle point p, the tangent map within the composition equals the successive tangent maps as above.

Русский

Для точки касательного пространства выполняется та же цепочка касательных отображений внутри композиции.

LaTeX

$$$\text{tangentMapWithin } I I'' (g \circ f) s p = \text{tangentMapWithin } I' I'' g u (\text{tangentMapWithin } I I' f s p).$$$

Lean4

theorem tangentMap_comp_at (p : TangentBundle I M) (hg : MDifferentiableAt I' I'' g (f p.1))
    (hf : MDifferentiableAt I I' f p.1) : tangentMap I I'' (g ∘ f) p = tangentMap I' I'' g (tangentMap I I' f p) :=
  by
  simp only [tangentMap, mfld_simps]
  rw [mfderiv_comp p.1 hg hf]
  rfl

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