Commit 2020-08-30 23:20 e88843ca
View on Github →feat(data/finset/sort): range_mono_of_fin (#3987)
Add a simp lemma giving the range of mono_of_fin.
feat(data/finset/sort): range_mono_of_fin (#3987)
Add a simp lemma giving the range of mono_of_fin.