Commit 2023-12-09 12:05 8fe6d2da

View on Github →

refactor(Gronwall): Restate in terms of LipschitzOnWith, EqOn (#8920) Restate the uniqueness theorems for solutions to ODEs using LipschitzOnWith and EqOn rather than the equivalent raw propositions, so that relevant APIs may be used for arguments of these theorems.

Estimated changes

Modified Mathlib/Analysis/ODE/Gronwall.lean

modified theorem ODE_solution_unique_of_mem_set

modified theorem dist_le_of_approx_trajectories_ODE_of_mem_set

modified theorem dist_le_of_trajectories_ODE_of_mem_set