Mathlib v3 is deprecated. Go to Mathlib v4

Theorem with_top.none_lt_some

Modification history

2020-09-26 02:31
src/order/bounded_lattice.lean
fix(order/bounded_lattice): fix some misleading theorem names (#4271)
Deleted with_top.none_lt_someView on Github →
2019-09-05 02:48
src/order/bounded_lattice.lean
feat(bounded_lattice/has_lt): add a `lt` relation independent from `l… (#1366) …
Added with_top.none_lt_someView on Github →