tangentMap_comp — Mathlib

English

As above, with p interpreted as a tangent bundle point in the given sets.

Русский

Как выше, при точке p как элемент касательного пространства в заданных множествах.

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 (hg : MDifferentiable I' I'' g) (hf : MDifferentiable I I' f) :
    tangentMap I I'' (g ∘ f) = tangentMap I' I'' g ∘ tangentMap I I' f := by ext p : 1;
  exact tangentMap_comp_at _ (hg _) (hf _)

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