Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-04 21:26 8a9a5d35

View on Github →

feat(dynamics): (semi-)flows, omega limits (#4843) This code has gone through a couple of iterations since it was first written in summer, when the ambition was 'Morse decompositions in Lean' rather than 'mildly generalise some results from a first course in differential equations'. Nevertheless there's much in here I'm not confident about & would appreciate help with.

Estimated changes

added theorem flow.ext
added def flow.from_iter
added theorem flow.image_eq_preimage
added theorem flow.map_add
added theorem flow.map_zero
added theorem flow.map_zero_apply
added def flow.restrict
added def flow.reverse
added structure flow
added def is_fw_invariant
added def is_invariant
added theorem is_invariant_iff_image
added theorem is_closed_omega_limit
added theorem maps_to_omega_limit'
added theorem maps_to_omega_limit
added theorem nonempty_omega_limit
added def omega_limit
added theorem omega_limit_Inter
added theorem omega_limit_Union
added theorem omega_limit_def
added theorem omega_limit_eq_Inter
added theorem omega_limit_image_eq
added theorem omega_limit_inter
added theorem omega_limit_mono_left
added theorem omega_limit_mono_right
added theorem omega_limit_union
added theorem continuous_curry