Louis Wasserman
Louis Wasserman
I think this version qualifies as finally having proved all the basic properties of multiplication of real numbers, but it will obviously need breaking up -- possibly even further than...
(Specifically, we have the ring laws, and we have that the standard embedding of rationals preserves multiplication.)
The monotone convergence theorem isn't unconditionally true constructively: it's equivalent to the [limited principle of omniscience](https://unimath.github.io/agda-unimath/foundation.limited-principle-of-omniscience.html). (See e.g. 1.2.1 in https://arxiv.org/abs/1804.05495 .)
From what I can tell from my research, proving sequences are Cauchy is far and away the most straightforward path to proving convergence in constructive settings, as in #1347. But...
> I really had the feeling that what you had written on the real numbers would unlock the supremum property and such. Unfortunately not. The supremum property is equivalent to...
I do feel obliged to mention that this has nonzero performance and memory costs, and I'd tend to include this in "best practices suggestions" rather than "hard rules" as a...
There might need to be additional continuity conditions on the ring operations. I have to admit I'm leaning more and more towards just naming the backing structure `Analysis-Setting`.
Restarting this.
Thinking further, I think we might as well go ahead and do the real function version to get us started; we will want the version of derivatives that is itself...
This does depend on #1740.