-
Notifications
You must be signed in to change notification settings - Fork 234
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - refactor(Gronwall): Restate in terms of LipschitzOnWith
, EqOn
#8920
Conversation
(hv : ∀ t, ∀ᵉ (x ∈ s t) (y ∈ s t), dist (v t x) (v t y) ≤ K * dist x y) | ||
theorem dist_le_of_approx_trajectories_ODE_of_mem_set {v : ℝ → E → E} {s : ℝ → Set E} {K : ℝ≥0} | ||
(hv : ∀ t, LipschitzOnWith K (v t) (s t)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Isn't the new statement weaker? You've demoted ∀ᵉ
to ∀
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Oh nevermind, I thought ∀ᵉ
was some special thing like eventually
, but it's just a weird notation for binders.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors merge
Thanks!
Build failed (retrying...): |
Pull request successfully merged into master. Build succeeded: |
LipschitzOnWith
, EqOn
LipschitzOnWith
, EqOn
Restate the uniqueness theorems for solutions to ODEs using
LipschitzOnWith
andEqOn
rather than the equivalent raw propositions, so that relevant APIs may be used for arguments of these theorems.