How about including this in the library? I don’t expect this library to actually use this theorem. Also, the proof doesn’t depend on any other parts of the ZornsLemma library. So it could as well be published on its own.
The only thing that uses things from ZornsLemma is an example, that every finite type is "omniscient".
Whether we include it or not, I need to clean up some bits (Print statements, comments).
I couldn’t avoid using extensionality axioms. The many ...' lemmas are there because I tried to find out where extensionality is necessary.
Also note, that N_infty can’t be replaced by option nat, without using more axioms.
Namely, the definition of the epsilon function fails, or at least needs
some non-trivial change.
Based on https://arxiv.org/abs/1904.09193. I thought, this theorem would be nice to formalize and give it some exposure.
How about including this in the library? I don’t expect this library to actually use this theorem. Also, the proof doesn’t depend on any other parts of the ZornsLemma library. So it could as well be published on its own. The only thing that uses things from ZornsLemma is an example, that every finite type is "omniscient". Whether we include it or not, I need to clean up some bits (Print statements, comments).
I couldn’t avoid using extensionality axioms. The many
...'lemmas are there because I tried to find out where extensionality is necessary. Also note, thatN_inftycan’t be replaced byoption nat, without using more axioms. Namely, the definition of the epsilon function fails, or at least needs some non-trivial change.