]> matita.cs.unibo.it Git - helm.git/tree - helm/software/matita/dama/
Bertrand's conjecture (weak), some work in progress
[helm.git] / helm / software / matita / dama /
drwxr-xr-x   ..
-rw-r--r-- 147 Makefile
-rw-r--r-- 6401 Q_is_orded_divisble_group.ma
-rw-r--r-- 125 TODO
drwxr-xr-x - attic
drwxr-xr-x - classical_pointfree
drwxr-xr-x - classical_pointwise
-rw-r--r-- 2236 constructive_connectives.ma
-rw-r--r-- 2253 constructive_higher_order_relations.ma
drwxr-xr-x - constructive_pointfree
-rw-r--r-- 1750 depends
-rw-r--r-- 3812 divisible_group.ma
drwxr-xr-x - doc
-rw-r--r-- 10411 excess.ma
-rw-r--r-- 8465 group.ma
-rw-r--r-- 6995 infsup.ma
-rw-r--r-- 11655 lattice.ma
-rw-r--r-- 5810 metric_lattice.ma
-rw-r--r-- 2710 metric_space.ma
-rw-r--r-- 3086 ordered_divisible_group.ma
-rw-r--r-- 11091 ordered_group.ma
-rw-r--r-- 3208 premetric_lattice.ma
-rw-r--r-- 13276 prevalued_lattice.ma
-rw-r--r-- 21 root
-rw-r--r-- 4242 sandwich.ma
-rw-r--r-- 2488 sandwich_corollary.ma
-rw-r--r-- 8592 sequence.ma