The sum of geometric series in the real numbers #1676
Conversation
…shake-out-signed-rational
…shake-out-signed-rational
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
src/elementary-number-theory/geometric-sequences-rational-numbers.lagda.md
Show resolved
Hide resolved
I'm not entirely sure about this atm either. I'll think a little about it. One question that comes to mind is, what was intended by the namespace name "analysis" if not also analysis of real numbers. Perhaps a fitting starting point would be to have "convergent sequences of real numbers" in the |
|
Perhaps we should do some planning |
|
One of the founding principles of the agda-unimath library is to organize modules by theory rather than data structure. Although, some of our namespaces don't reflect this principle that well these days, such as |
…lagda.md Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
src/commutative-algebra/geometric-sequences-commutative-rings.lagda.md
Outdated
Show resolved
Hide resolved
src/real-numbers/uniformly-continuous-functions-real-numbers.lagda.md
Outdated
Show resolved
Hide resolved
src/real-numbers/uniformly-continuous-functions-real-numbers.lagda.md
Outdated
Show resolved
Hide resolved
Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
We turn out to need the locatedness condition to prove this is an apartness relation, but that suffices, and we go on to prove that apartness in the real numbers is equivalent. Builds on some of the apartness work done in #1676 .
2 participants
Builds on #1675, #1673, and #1672. Completes #1605.