analysis icon indicating copy to clipboard operation
analysis copied to clipboard
verified publisher icon math-comp

WIP: Rewriting countability and finiteness

Open CohenCyril opened this issue 7 years ago • 2 comments

countability and finiteness now share the interface of countType and finType through the coercions countable >-> Sortclass and finite >-> Sortclass e.g. rpickle c is replaced by @pickle [countType of c] where c : countable E. Additionally, sketching lemmas about combining infinite, finite and cofinite sets.

This is a draft, it does not compile anymore, but it sketches improvements of countability theory.

CohenCyril avatar Apr 25 '18 21:04 CohenCyril

memo: mentioned in PR #294

affeldt-aist avatar May 12 '21 02:05 affeldt-aist

partially handed by PR #435?

affeldt-aist avatar Oct 04 '21 03:10 affeldt-aist