Definition of regular continued fractions

Stream: mathlib4

[Miyahara Kō]

In mathlib, a regular continued fraction is defined as a simple continued fraction whose partial denominators are all positive, but no matter which literature I searched, a regular continued fraction is defined as a simple continued fraction whose head term is integer and whose partial denominators are all positive naturals. Indeed, if we redefine a regular continued fraction as this way, we can get correspondence between reals and regular continued fractions which does't finish with 1. I want to redefine regular continued fractions.

[Miyahara Kō]

I'm constructing the homeomorphism between irrationals and Baire space using continued fractions.
Partial result can be seen in Komyyy/PFunctor.M branch.

[Miyahara Kō]

Sorry for the lack of updates due to mental problems over the past 5 months.
In the proof of showing that a continued fraction and a veil space are isomorphic, I noticed that the continued fraction is used a lot of extra induction as potentially infinite sequences, and I felt that Lean's current type system is inconvenient because of the lack of coinductive types. In addition, there are some drawbacks such as timeout due to simplification of proof terms, non-stoppage of simplification by removing subsingletons, and breaking of subject reduction by considering quotient types of propositions, so, prior to proving isomorphism, I first wanted to find a type system that improves on these issues for my graduation thesis.
Therefore, this project is temporarily frozen. The related PR will also be closed (I will keep the branch as it may be revived someday).