Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-26 02:31 6289adfc

View on Github →

fix(order/bounded_lattice): fix some misleading theorem names (#4271)

Estimated changes

modified theorem with_top.coe_lt_top
added theorem with_top.le_none
deleted theorem with_top.none_le
deleted theorem with_top.none_lt_some
added theorem with_top.some_lt_none