Commit 2023-02-23 08:00 4375498b

View on Github →

feat: Port Dynamics.Flow (#2451)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/Flow.lean

added theorem Flow.continuous_toFun

added theorem Flow.ext

added def Flow.fromIter

added theorem Flow.image_eq_preimage

added theorem Flow.isInvariant_iff_image_eq

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 def Flow.toHomeomorph

added structure Flow

added theorem IsFwInvariant.isInvariant

added def IsFwInvariant

added theorem IsInvariant.isFwInvariant

added def IsInvariant

added theorem isFwInvariant_iff_isInvariant

added theorem isInvariant_iff_image