]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 92682f0) | 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)
commit08d8e4e422aafdc11e4230a87f2adee7facad809
treecae065cbc722b198f355bf7b4d8aa4b01f67bbf6tree | snapshot
parent92682f04ee34e7fb98ee5311646aaa62838f1e17commit | 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).
matita/dama/groups.ma diff | blob | history
matita/dama/integration_algebras.ma diff | blob | history
matita/dama/reals.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.