Radial contractions preserve orientation at their centre #
A radial contraction of a finite-dimensional real normed space E fixes its centre, and its
derivative there is the identity. So it preserves every orientation of E at its centre
(TauCeti.isOrientationPreservingAt_radialContraction_self).
Main results #
TauCeti.isOrientationPreservingAt_radialContraction_self: a radial contraction preserves every orientation ofEat its centre.
theorem
TauCeti.isOrientationPreservingAt_radialContraction_self
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{ι : Type u_2}
[Fintype ι]
(o : Manifold.Orientation (modelWithCornersSelf ℝ E) E ι)
(c : E)
(κ : ℝ)
:
o.IsOrientationPreservingAt o (radialContraction c κ) c
A radial contraction preserves every orientation of E at its centre.