Louis Wasserman
Louis Wasserman
We do something more general, actually, which is show that any strictly increasing, pointwise continuous, unbounded function from ℝ to ℝ is an equivalence.
This is [Formalizing 100 Theorems](https://www.cs.ru.nl/~freek/100/) number 38. I observe we already have it for rational numbers, and maybe we can count it? Some of the other examples definitely focus on...
Setting up for #1471, though I'm not yet certain about the right strategy to prove it -- all the proofs on Wikipedia use casework on whether the elements of the...
As promised, we combine square roots and odd roots to make arbitrary natural roots, which will allow us to define arbitrary rational roots.
Classical analysis defines the word "continuity" by itself as pointwise continuity. Bishop, and some other constructive analysis texts I've read, use a different definition of "continuous function" that is classically...
Still getting a handle on how we like to work with coinductive records, though the conatural numbers are an example I'm taking notes from.
Theorem 22 of the 100 Theorems. This seems like a pain, but only a pain.
Theorem 64 of the 100 Theorems. Should be doable enough once we have derivatives -- though we'll need to define derivatives on the entire real line, not just on proper...