Takafumi Saikawa
Takafumi Saikawa
anyway this PR should be merged quickly
> anyway this PR should be merged quickly @affeldt-aist ping?
It seems I have had some rights.
Why not parallelly formalize Fsigma sets too? (renaming the file to borel_hierarchy.v)
like this https://github.com/affeldt-aist/analysis/pull/40/
It looks short but a nice place for future additions, e.g., a generic definition of the borel hierarchy parametrized by a well-ordered set. Btw, there will be another demand for...
(Can I push to this repository once I drop a comment here?)
(nope)
rebased
As #183 is updated and merged, I have tried to rebase this branch over master again, but the divergence has become larger than I expected. Can you handle this? @affeldt-aist