The actual tangent map of closed-ball inclusion

Closed-ball charts are restrictions of inversion charts. Their inverse derivatives are invertible even at the sphere, giving the actual inclusion a tangent equivalence everywhere. In particular the derivative of the inclusion is injective at every point.

noncomputable def TauCeti.subtypeValClosedBallTangentEquiv {n : ℕ} [NeZero n] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = n)] (x : ↑(Metric.closedBall 0 1)) : TangentSpace (modelWithCornersEuclideanHalfSpace n) x ≃L[ℝ] V

The actual inclusion derivative of a closed unit ball is an invertible tangent map, including at every point of its sphere boundary.

@[simp]

theorem TauCeti.subtypeValClosedBallTangentEquiv_toContinuousLinearMap {n : ℕ} [NeZero n] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = n)] (x : ↑(Metric.closedBall 0 1)) : ↑(subtypeValClosedBallTangentEquiv x) = ↑(NormedSpace.fromTangentSpace ↑x) ∘SL mfderiv% Subtype.val x

The tangent equivalence is precisely the actual inclusion derivative after the canonical normed-model tangent identification.

theorem TauCeti.injective_mfderiv_subtypeVal_closedBall {n : ℕ} [NeZero n] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = n)] (y : ↑(Metric.closedBall 0 1)) : Function.Injective ⇑(mfderiv% Subtype.val y)

The inclusion of the closed unit ball has an injective derivative at every point, including at the points of its boundary sphere.