mathlib3
0716fa44 - feat(data/set/intervals/basic): not_mem of various intervals (#6238)

Commit
4 years ago
feat(data/set/intervals/basic): not_mem of various intervals (#6238) `c` is not in a given open/closed/unordered interval if it is outside the bounds of that interval (or if it is not in a superset of that interval).
Parents
Loading