differentiable_within_at_localInvariantProp

theorem differentiable_within_at_localInvariantProp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {E' : Type u_5} [inst_4 : NormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_6 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H'), (contDiffGroupoid ⊤ I).LocalInvariantProp (contDiffGroupoid ⊤ I') (DifferentiableWithinAtProp I I')

This theorem states that the property of being differentiable within a certain region in a model space is a local property that is invariant under smooth mappings. Consequently, this property can be smoothly transferred to manifolds. The theorem holds for all relevant types and instances, including nontrivially normed fields, normed additive commutative groups, normed spaces, topological spaces, and models with corners.

More concisely: The property of differentiability is a local property invariant under smooth mappings and can be transferred between compatible manifolds in models of various types, including normed fields, normed groups, normed spaces, topological spaces, and models with corners.