Theorem directedOn_le_Iic

Modification history

2026-09-08 16:08
Mathlib/Order/Interval/Set/Image.lean
chore(Order/Interval/Set/Image): use `to_dual` (#43584)
Modified directedOn_le_IicView on Github →
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_le_IicView on Github →