]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7270b6b) | patch
- A new interesting elimination principle over inductively generated topologies:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 4 Nov 2008 10:22:30 +0000 (10:22 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 4 Nov 2008 10:22:30 +0000 (10:22 +0000)
commit13f687d1d7cc07a19dcf28e1624f78a3a9d9c840
tree77d7ff5f914268f67b84235e47d823d31a7e85f4tree | snapshot
parent7270b6b325f031944a732c9561986988d0dddcf0commit | diff
- A new interesting elimination principle over inductively generated topologies:
  the elimination principle for general topologies hold!
- A proof of Cantor theorem using formal topologies. By Silvio Valentini.
helm/software/matita/library/demo/cantor.ma [new file with mode: 0644] blob
helm/software/matita/library/demo/formal_topology.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.