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

theorem AVenhance.flow_isFlow (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‖) : IsFlow b (flow b hb hL)

Characterization: flow satisfies the flow equation and initial condition.