]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d61b0ec) | patch
More work on groups, real numbers and integration algebras.
authorEnrico Zoli <??>
Mon, 6 Nov 2006 18:43:24 +0000 (18:43 +0000)
committerEnrico Zoli <??>
Mon, 6 Nov 2006 18:43:24 +0000 (18:43 +0000)
commit96d238f03dd89a1a04b1e9ccc06b476482eaf754
tree1ce2551578a80e6b23b8367b90a081fb026781b8tree | snapshot
parentd61b0ec37e7943a058dc9c6381efe49db7eb575fcommit | diff
More work on groups, real numbers and integration algebras.
Up to a thousand of unproved lemmas, we have the result that the
distance induced by the integral on an integration Riesz space is
a distance. The next step is to axiomatise an L-space (an integration
Riesz space complete w.r.t. the induced distance).
helm/software/matita/dama/groups.ma diff | blob | history
helm/software/matita/dama/integration_algebras.ma diff | blob | history
helm/software/matita/dama/reals.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.