Equality of actual cylinder L² slices identifies their continuous representatives everywhere.

theorem EulerCylinderSmoothOrbit.pointField_eq_of_slice_eq (P : ℝ) [Fact (0 < P)] {K : Type u_1} {L : Type u_2} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (q : C(L, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (t : K) (s : L) (he : p t = q s) : pointField P p hp t = pointField P q hq s

theorem EulerCylinderSmoothOrbit.scalarPointField_eq_of_slice_eq (P : ℝ) [Fact (0 < P)] {K : Type u_1} {L : Type u_2} [TopologicalSpace K] [CompactSpace K] [TopologicalSpace L] [CompactSpace L] (p : C(K, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (q : C(L, ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (t : K) (s : L) (he : p t = q s) : EulerCylinderScalarPrimitive.scalarPointField P p hp t = EulerCylinderScalarPrimitive.scalarPointField P q hq s