Commit 2022-12-20 13:26 893f77fc

View on Github →

feat: port Dynamics.Basic (#1120)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Dynamics/Basic.lean

added theorem Function.Commute.invOn_fixedPoints_comp

added theorem Function.Commute.left_bijOn_fixedPoints_comp

added theorem Function.Commute.right_bijOn_fixedPoints_comp

added theorem Function.Injective.isFixedPt_apply_iff

added theorem Function.IsFixedPt.left_of_comp

added theorem Function.IsFixedPt.preimage_iterate

added theorem Function.IsFixedPt.to_leftInverse

added def Function.IsFixedPt

added theorem Function.Semiconj.maps_to_fixedPoints

added theorem Function.bijOn_fixedPoints_comp

added def Function.fixedPoints

added theorem Function.fixedPoints_id

added theorem Function.fixedPoints_subset_range

added theorem Function.invOn_fixedPoints_comp

added theorem Function.isFixedPt_id

added theorem Function.maps_to_fixedPoints_comp

added theorem Function.mem_fixedPoints

added theorem Function.mem_fixedPoints_iff

Modified Mathlib/Logic/Equiv/Defs.lean

added theorem Equiv.leftInverse_symm

deleted theorem Equiv.left_inverse_symm

added theorem Equiv.rightInverse_symm

deleted theorem Equiv.right_inverse_symm

Modified Mathlib/Logic/Equiv/Set.lean