Mathlib v3 is deprecated. Go to Mathlib v4

Theorem int.cInf_of_not_bdd_below

Modification history

2022-11-05 21:51

src/data/int/conditionally_complete_order.lean

chore(data/int/basic): split file (#17342) …

Modified int.cInf_of_not_bdd_below View on Github →

2021-07-13 21:48

src/data/int/order.lean

feat(data/int): conditionally complete linear order (#8149) …

Added int.cInf_of_not_bdd_below View on Github →