]> matita.cs.unibo.it Git - helm.git/commit
Dama: up to L-spaces and the proof (completed up to properties of the
authorEnrico Zoli <??>
Fri, 10 Nov 2006 18:06:13 +0000 (18:06 +0000)
committerEnrico Zoli <??>
Fri, 10 Nov 2006 18:06:13 +0000 (18:06 +0000)
commit00f8600ea6678e2e2e343df1edc4877c3abcfef8
tree7291c204ba9fa0eb6287159267e9eb3e52f9bd2c
parent96d238f03dd89a1a04b1e9ccc06b476482eaf754
Dama: up to L-spaces and the proof (completed up to properties of the
absolute value) that every complete integration riesz space is an L-space.
Now the plan is to prove the Lebesgue dominated convergence theorem for
L-spaces as Fremlin does and to build a model of them later on as suggested
by Spitters. Note: the proof of the theorem by Spitters is almost trivial
because it really exploits the fact the L0 is the (Cauchy) completion of L1.
The proof by Fremlin is much more general since it does not assume anything
more on L-spaces.

Note: we could also prove that every L-space is archimedean.
helm/software/matita/dama/integration_algebras.ma
helm/software/matita/dama/vector_spaces.ma [new file with mode: 0644]