Proper separation of vector spaces: vanilla, metric, normed, and Euclidean
Showing
- current-formalism/Convergence/Impossibility_2G_1B.v 32 additions, 29 deletionscurrent-formalism/Convergence/Impossibility_2G_1B.v
- current-formalism/Core/Formalism.v 2 additions, 1 deletioncurrent-formalism/Core/Formalism.v
- current-formalism/Gathering/Definitions.v 1 addition, 0 deletionscurrent-formalism/Gathering/Definitions.v
- current-formalism/Gathering/Impossibility.v 883 additions, 806 deletionscurrent-formalism/Gathering/Impossibility.v
- current-formalism/Gathering/InR/Algorithm.v 14 additions, 11 deletionscurrent-formalism/Gathering/InR/Algorithm.v
- current-formalism/Gathering/InR/Impossibility.v 4 additions, 2 deletionscurrent-formalism/Gathering/InR/Impossibility.v
- current-formalism/Gathering/InR2/Algorithm.v 7 additions, 4 deletionscurrent-formalism/Gathering/InR2/Algorithm.v
- current-formalism/Gathering/WithMultiplicity.v 2 additions, 0 deletionscurrent-formalism/Gathering/WithMultiplicity.v
- current-formalism/Models/Flexible.v 1 addition, 0 deletionscurrent-formalism/Models/Flexible.v
- current-formalism/Models/Similarity.v 2 additions, 1 deletioncurrent-formalism/Models/Similarity.v
- current-formalism/Spaces/EuclideanSpace.v 313 additions, 0 deletionscurrent-formalism/Spaces/EuclideanSpace.v
- current-formalism/Spaces/R.v 33 additions, 74 deletionscurrent-formalism/Spaces/R.v
- current-formalism/Spaces/R2.v 295 additions, 637 deletionscurrent-formalism/Spaces/R2.v
- current-formalism/Spaces/RealMetricSpace.v 7 additions, 143 deletionscurrent-formalism/Spaces/RealMetricSpace.v
- current-formalism/Spaces/RealNormedSpace.v 197 additions, 0 deletionscurrent-formalism/Spaces/RealNormedSpace.v
- current-formalism/Spaces/RealVectorSpace.v 167 additions, 0 deletionscurrent-formalism/Spaces/RealVectorSpace.v
- current-formalism/Spaces/Similarity.v 141 additions, 65 deletionscurrent-formalism/Spaces/Similarity.v
- current-formalism/Spectra/LimitedMultisetSpectrum.v 2 additions, 1 deletioncurrent-formalism/Spectra/LimitedMultisetSpectrum.v
- current-formalism/Spectra/LimitedSetSpectrum.v 2 additions, 1 deletioncurrent-formalism/Spectra/LimitedSetSpectrum.v
- current-formalism/Spectra/MultisetSpectrum.v 3 additions, 2 deletionscurrent-formalism/Spectra/MultisetSpectrum.v
Loading
Please register or sign in to comment