Commit 2020-07-21 11:50 5c55e157
View on Github →feat(data/finset/intervals): Lemma about filter and Ico (#3479) Add "if you filter an Ico based on being less than or equal to its bottom element, you get the singleton bottom element".
feat(data/finset/intervals): Lemma about filter and Ico (#3479) Add "if you filter an Ico based on being less than or equal to its bottom element, you get the singleton bottom element".