basic): lemmas about `(range n).nonempty` (#8905)

Commit

4 years ago

chore(data/finset/basic): lemmas about `(range n).nonempty` (#8905) Add `finset.nonempty_range_iff`, `finset.range_eq_empty_iff`, and `range.nonempty_range_succ`.

Author

urkud

Parents

1e89df22

mathlib3 b3807ee3 - chore(data/finset/basic): lemmas about `(range n).nonempty` (#8905)

mathlib3
b3807ee3 - chore(data/finset/basic): lemmas about `(range n).nonempty` (#8905)