sort): range_mono_of_fin (#3987)

Commit

5 years ago

feat(data/finset/sort): range_mono_of_fin (#3987) Add a `simp` lemma giving the range of `mono_of_fin`.

References

Author

jsm28

Parents