Derivatives of maps into a closed subspace

If the increments f y - f x of a map lie in a closed subspace S for y near x, that is, if f takes its values in the affine subspace f x + S near x, then its derivative at x takes values in S: the difference quotients lie in S, and so does their limit. This is what shows that the Lie bracket of two vector fields tangent to a fixed subspace is again tangent to it.

theorem HasFDerivAt.apply_mem_of_eventually_sub_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {S : Submodule 𝕜 F} (hf : HasFDerivAt f f' x) (hS : IsClosed ↑S) (hfS : ∀ᶠ (y : E) in nhds x, f y - f x ∈ S) (v : E) : f' v ∈ S

If f has derivative f' at x and its increments f y - f x lie in the closed subspace S for y near x, then f' takes values in S.

theorem TauCeti.fderiv_apply_mem_of_eventually_sub_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {S : Submodule 𝕜 F} (hS : IsClosed ↑S) (hfS : ∀ᶠ (y : E) in nhds x, f y - f x ∈ S) (v : E) : (fderiv 𝕜 f x) v ∈ S

If the increments f y - f x lie in the closed subspace S for y near x, then the derivative of f at x takes values in S.