Commit 2024-02-13 15:17 95eca4bb

View on Github →

feat(Topology/Algebra/Order): continuous injective function on interval is strictly monotone (#7018) Suppose f : [a, b] → δ or f : (a, b) → δ is continuous and injective. Then f is strictly monotone.

Estimated changes

Modified Mathlib/Data/Set/Intervals/Image.lean

added theorem directedOn_ge_Icc

added theorem directedOn_ge_Ici

added theorem directedOn_ge_Ico

added theorem directedOn_le_Icc

added theorem directedOn_le_Iic

added theorem directedOn_le_Ioc

Modified Mathlib/Order/Antichain.lean

added theorem IsAntichain.of_monotoneOn_strictAntiOn

added theorem IsAntichain.of_strictMonoOn_antitoneOn

Modified Mathlib/Order/Directed.lean

added theorem constant_of_monotoneOn_antitoneOn

added theorem constant_of_monotone_antitone

Modified Mathlib/Topology/Algebra/Order/IntermediateValue.lean

added theorem Continuous.strictAnti_of_inj_boundedOrder

added theorem Continuous.strictMonoOn_of_inj_rigidity

added theorem Continuous.strictMono_of_inj

added theorem Continuous.strictMono_of_inj_boundedOrder'

added theorem Continuous.strictMono_of_inj_boundedOrder

added theorem ContinuousOn.strictAntiOn_of_injOn_Icc

added theorem ContinuousOn.strictMonoOn_of_injOn_Icc'

added theorem ContinuousOn.strictMonoOn_of_injOn_Icc

added theorem ContinuousOn.strictMonoOn_of_injOn_Ioo