Commit 2021-06-11 13:26 915a0a21
View on Github →feat(topology/algebra/ordered/basic): add a few subseq-related lemmas (#7828) These are lemmas I proved while working on #7164. Some of them are actually not used anymore in that PR because I'm refactoring it, but I thought they would be useful anyway, so here there are.