Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-05 02:48 28549094

View on Github →

feat(bounded_lattice/has_lt): add a lt relation independent from `l… (#1366)

  • feat(bounded_lattice/has_lt): add a lt relation independent from le for has_top
  • use priority 10 instead of 0

Estimated changes

added theorem with_top.none_le
added theorem with_top.none_lt_some
modified theorem with_top.some_le_some
modified theorem with_top.some_lt_some