Commit 2024-08-01 10:24 0139a899

View on Github →

feat(IntermediateValue): add IsFixedPt corollaries (#15395) Motivated by https://github.com/b-mehta/sharkovsky Also move the definition of Function.IsFixedPt to Logic/Function/Defs.

Estimated changes

Modified Mathlib/Dynamics/FixedPoints/Basic.lean

deleted def Function.IsFixedPt

Modified Mathlib/Logic/Function/Defs.lean

added def Function.IsFixedPt

Modified Mathlib/Topology/Order/IntermediateValue.lean

added theorem exists_mem_Icc_isFixedPt

added theorem exists_mem_Icc_isFixedPt_of_mapsTo

added theorem exists_mem_uIcc_isFixedPt

modified theorem intermediate_value_uIcc

modified theorem isPreconnected_uIcc