Theorem directedOn_ge_Ico

Modification history

2024-02-13 15:17
Mathlib/Data/Set/Intervals/Image.lean
feat(Topology/Algebra/Order): continuous injective function on interval is strictly monotone (#7018) …
Added directedOn_ge_IcoView on Github →