Mathlib v3 is deprecated. Go to Mathlib v4

Theorem no_top

Modification history

2022-01-11 13:55
src/order/basic.lean
chore(order/basic): Rename `no_bot_order`/`no_top_order` to `no_min_order`/`no_max_order` (#11357) …
Deleted no_topView on Github →
2021-12-14 05:36
src/order/basic.lean
feat(order/basic, order/bounded_order): Generalized `preorder` to `has_lt` (#10695) …
Modified no_topView on Github →
2021-07-19 07:28
src/order/basic.lean
chore(order/basic): whitespaces and caps (#8359)
Modified no_topView on Github →
2017-08-26 15:40
order/basic.lean
feat(topology): port metric space from lean2
Added no_topView on Github →