Lemmas about the reals - Githubissues

Smaug123 / agdaproofs

Mathematical proofs in Agda

MIT License

4 stars 1 forks source link

Lemmas about the reals #96

Open Smaug123 opened 4 years ago

Smaug123 commented 4 years ago

Lots of these are badly organised - e.g. stuff about limits of real sequences is actually true of any totally ordered field of characteristic != 2. Split them out properly.