Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-14 18:39 084b7e7d

View on Github →

chore(algebra/order,data/set/intervals): a few more trivial lemmas (#4611)

  • a few more lemmas for has_le.le and has_lt.lt namespaces;
  • a few lemmas about intersections of intervals;
  • fix section header in topology/algebra/module.

Estimated changes

added theorem has_le.le.le_or_le
modified theorem has_le.le.le_or_lt
modified theorem has_le.le.lt_or_le
added theorem has_lt.lt.lt_or_lt
added theorem has_lt.lt.ne'