The adjoint of the genuine mixed cylinder translation is its inverse.

theorem EulerLpCylinderTranslation.translate_adjoint (P : ℝ) [Fact (0 < P)] {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (a : EulerLiftedGradientSpace.LiftTangent) : ContinuousLinearMap.adjoint (translate P a).toContinuousLinearMap = (translate P (-a)).toContinuousLinearMap

theorem EulerTimeLpBoundedMap.pathLp_timeLift {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (T : ℝ) (hT : 0 ≤ T) (A : E →L[ℝ] F) (f : C(↑(Set.Icc 0 T), E)) : EulerTimeLp.pathLp T hT ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 T)) A) f) = (timeLift T A) (EulerTimeLp.pathLp T hT f)

The actual continuous-time embedding commutes with bounded spatial maps.