Orientations of closed unit balls

The inclusion tangent equivalence transports any orientation of a positive-dimensional real inner-product space to its closed unit ball, including at every boundary point.

noncomputable def TauCeti.Manifold.Orientation.closedBall {n : ℕ} [NeZero n] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = n)] (o : _root_.Orientation ℝ V (Fin n)) : Orientation (modelWithCornersEuclideanHalfSpace n) (↑(Metric.closedBall 0 1)) (Fin n)

The closed unit ball's orientation induced by its inclusion derivative.

@[simp]

theorem TauCeti.Manifold.Orientation.map_orientationAt_closedBall {n : ℕ} [NeZero n] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = n)] (o : _root_.Orientation ℝ V (Fin n)) (x : ↑(Metric.closedBall 0 1)) : (Orientation.map (Fin n) ↑(subtypeValClosedBallTangentEquiv x)) ((closedBall o).orientationAt x) = o

At every point of the ball, its inclusion tangent equivalence preserves the chosen ambient orientation. This also holds at the sphere boundary and in dimension one.

theorem TauCeti.orientable_closedBall {n : ℕ} [NeZero n] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (Module.finrank ℝ V = n)] : Orientable (modelWithCornersEuclideanHalfSpace n) ↑(Metric.closedBall 0 1)

Every positive-dimensional closed unit ball is orientable, including dimension one.