English
A tangent map within the composition equals the composed tangent maps in the expected order: tangentMapWithin I I'' (g ∘ f) s p = tangentMapWithin I' I'' g u (tangentMapWithin I I' f s 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
/-- Predicate ensuring that, at a point and within a set, a function can have at most one
derivative. This is expressed using the preferred chart at the considered point. -/
def UniqueMDiffWithinAt (s : Set M) (x : M) :=
UniqueDiffWithinAt 𝕜 ((extChartAt I x).symm ⁻¹' s ∩ range I) ((extChartAt I x) x)
