Theorem Continuous.strictMonoOn_of_inj_rigidity

Modification history

2024-02-13 15:17
Mathlib/Topology/Algebra/Order/IntermediateValue.lean
feat(Topology/Algebra/Order): continuous injective function on interval is strictly monotone (#7018) …
Added Continuous.strictMonoOn_of_inj_rigidityView on Github →