zstone1
zstone1
##### Motivation for this change Splitting out another piece of the Banach Fixed Point PR, this just defines contractions and proves a simple fact about them. Note that this places...
I'm encountering some issues with certain applications of the `near` tactics. One set of issues is getting instances of `\near F, ...` to typecheck. The example that I encountered was...
In the spirit of giving real-world reproductions, rather than minimal ones, here's a failed attempt from the arzela ascoli proofs. I proved ``` Lemma small_ent_split {Y : uniformType} (E :...
##### Motivation for this change A generally useful result that doesn't require any machinery beyond geometric series. The proof is not too long, thankfully. 1. There is some nasty geometric...
Long story short, I want to work with modules over the complex numbers, but have the norms live in the real numbers. Things like `infs` and `sups` are defined only...
##### Motivation for this change My medium term goal is to prove stuff about the cantor space. One important feature of the space is that it is metrizable. It is...
##### Motivation for this change The cantor set is generally useful construction, but not particularly general or easy to formalize. Instead we do most the theory using the "cantor space",...
I've done a review of the fsbigop.v file. Looks pretty reasonable. There are a couple mechanical things, and then a couple more general questions: @affeldt-aist, not sure who else should...
I get a weird error message after completing a `near` proof, but before Unshelving: > TypeError: Cannot read property 'before' of null Not sure what it's talking about, and everything...
Hello, I'm having a problem with scala versions. I'm trying to use KeymaeraX as a library (I want the parser, printer, expression subsitution, ect. All stuff from core). But I'm...