Commit 2023-10-24 07:55 f201111e
View on Github →fix: Incorrect integral curve existence theorem for vector fields (#6875)
exists_isPicardLindelof_const_of_contDiffOn_nhds had unnecessarily specific assumptions.
ContDiffOn assumption is replaced with ContDiffAt.
ProperSpace E assumption is removed.