I created a pr https://github.com/math-comp/analysis/pull/206
Can I move my message to a specific topic ?
For bookeeping
Done, and sorry I forgot to answer
No problem
I updated the PR, it has top/bottom/sub/complement
oops I didn't see the extra proper_neqAsubset
I added the lemma proper_neqAsubset.
Is there a other improvement I can do for the pr ?
thanks for the review!
Last updated: Feb 09 2023 at 03:06 UTC