zstone1
zstone1
Is there any plan for syntactic support for vectors and matrices in KeYmaera? I've got a non-trivial matlab algorithm that I want to encode in a hybrid program. It uses...
##### Motivation for this change ----- Overall goal ----- More cantor space helper theorems. The overall goal is to prove that, for countable `I`, `I -> C` is homeomorphic to...
Notations like `{within A, continuous f}` that specialize a common one (E.G. `continuous f`) don't print correctly. For a full list, `{within A, continuous f}` prints as `continuous f` `{...
The `\o` and `^-1` operation used in entourages are instances of a much more general "relation composition". We should add this notion to classical_sets, build its theory. There are several...
The following code has an error (when "JustPath" is commented out). ``` (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrint...
##### Motivation for this change Finally, we prove that countable products of metrics are metrizable! In particularly, the cantor set is metrizable. I have - A definition for `countable_uniformity`. Several...
##### Motivation for this change Paths and loops are a critical feature of complex analysis. So we get started here with some basic definitions. Note this is still in draft...
As required by @CohenCyril in math-comp/analysis#750, I have a substantially minified example here: ``` From mathcomp Require Import all_ssreflect. From HB Require Import structures. HB.mixin Record IsX {T: Type} (f...
Something came up in the last mathcomp analysis meeting regarding `homo` vs `mono` in Order.v. For a function `f` between partial orders, saying `{mono f : x y / x
##### Motivation for this change Three important changes here. 1. The `topology.v` file is huge, and kinda unpleasant for development. This splits all the function space topology stuff into a...