coPset: some lemmas about infinity

Proofs by Joshua Yanowski

added 1 commit

• 634f461c - coPset: some lemmas about infinity

Compare with previous version

added 1 commit

• 94e85fef - coPset: some lemmas about infinity

Compare with previous version

added 5 commits

• b5798e60 - Add lemma `list_to_set_finite`.
• 2782152e - Add lemma `top_infinite`.
• e8ac5908 - Improve comment about `coPpick`.
• b390cc24 - Results about `set_infinite` on `coPset`.
• 60c6845c - coPset: some lemmas about infinity

Compare with previous version

It turned out that coPpick could be used to prove these lemmas. I have refactored the proofs and pushed.

Also the lemma about ⊤ could be generalized to any set with a top element.

Sure, that also works for me. :) Thanks for the simplification!

Also the lemma about ⊤ could be generalized to any set with a top element.

Ah, I was hoping something like this would be possible, nice.

merged

mentioned in commit 9a0f8631

Great, merging then! Thanks for the MR.