Statement file: flowInv_leftInverse (FlowDefs). This file contains exactly one declaration of the formalization's public statement surface.

theorem AVenhance.flowInv_leftInverse (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hb : Continuous fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (hL : ∃ (L : ℝ), ∀ (t : ℝ) (x y : Homogenization.Vec 2), ‖b t x - b t y‖ ≤ L * ‖x - y‖) (t s : ℝ) : Function.LeftInverse (fun (y : Homogenization.Vec 2) => flowInv b hb hL t y s) fun (x : Homogenization.Vec 2) => flow b hb hL t x s

Characterization: flowInv t · s is a left inverse of flow t · s.