Mathlib v3 is deprecated. Go to Mathlib v4

Theorem le_iff_le_iff_lt_iff_lt

Modification history

2021-10-08 07:33

src/algebra/order/basic.lean

move(order/*): move from `algebra.order.` the files that aren't about algebra (#9562) …

Modified le_iff_le_iff_lt_iff_lt View on Github →

2017-12-21 06:51

algebra/order.lean

feat(data/ordinal): omega is least limit ordinal

Modified le_iff_le_iff_lt_iff_lt View on Github →

2017-09-16 02:53

algebra/order.lean

feat(algebra): new algebra theorems (more iff)

Added le_iff_le_iff_lt_iff_lt View on Github →