Tangent cones of linear subspaces and of curves

Two basic facts about Mathlib's tangent cone tangentConeAt. The subspace calculation lets flattening charts identify their model subspaces with intrinsic tangent spaces, while the curve lemma places velocities of invariant flows in the tangent cones of their invariant sets.

Main results

• Submodule.tangentConeAt_eq: the tangent cone of a closed subspace at one of its points is the subspace itself.
• HasDerivAt.mem_tangentConeAt: the velocity of a curve lying in a set is tangent to the set.

theorem Submodule.tangentConeAt_eq {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (L : Submodule 𝕜 E) (hL : IsClosed ↑L) {x : E} (hx : x ∈ L) : tangentConeAt 𝕜 (↑L) x = ↑L

The tangent cone of a closed linear subspace at one of its points is the subspace itself.

theorem HasDerivAt.mem_tangentConeAt {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {γ : 𝕜 → E} {v : E} {t : 𝕜} {S : Set E} (hγ : HasDerivAt γ v t) (hS : ∀ᶠ (s : 𝕜) in nhds t, γ s ∈ S) : v ∈ tangentConeAt 𝕜 S (γ t)

The velocity of a curve which stays in a set S near time t lies in the tangent cone of S at the point reached at time t.