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

theorem AVenhance.existsUnique_flow (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‖) : ∃! X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2, IsFlow b X

Global well-posedness of the flow for continuous, uniformly globally Lipschitz fields.