The fixed-time maps of a smooth flow are C¹ inverses.

theorem AVenhance.Infra.Flow.flow_fixed_time_maps_are_C1_inverses {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s t : ℝ) : (ContDiff ℝ 1 fun (x : Homogenization.Vec 2) => X t x s) ∧ (ContDiff ℝ 1 fun (x : Homogenization.Vec 2) => X s x t) ∧ (∀ (x : Homogenization.Vec 2), X s (X t x s) t = x) ∧ ∀ (x : Homogenization.Vec 2), X t (X s x t) s = x

For each pair of times, the two spatial flow maps are continuously differentiable inverses of one another.