]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/dama/depends
Bertrand's conjecture (weak), some work in progress
[helm.git] / helm / software / matita / dama / depends
1 metric_lattice.ma excess.ma lattice.ma metric_space.ma
2 metric_space.ma ordered_divisible_group.ma
3 sandwich.ma metric_lattice.ma nat/orders.ma nat/plus.ma sequence.ma
4 premetric_lattice.ma lattice.ma metric_space.ma
5 ordered_group.ma group.ma
6 divisible_group.ma group.ma nat/orders.ma
7 ordered_divisible_group.ma divisible_group.ma nat/orders.ma nat/times.ma ordered_group.ma
8 sequence.ma excess.ma nat/orders.ma ordered_group.ma
9 constructive_connectives.ma logic/connectives.ma
10 lattice.TF.ma excess.ma lattice.ma nat/nat.ma
11 group.ma excess.ma
12 prevalued_lattice.ma ordered_group.ma
13 excess.ma constructive_connectives.ma constructive_higher_order_relations.ma higher_order_defs/relations.ma nat/plus.ma
14 sandwich_corollary.ma metric_lattice.ma sandwich.ma
15 Q_is_orded_divisble_group.ma Q/q.ma ordered_divisible_group.ma
16 lattice.ma excess.ma
17 constructive_higher_order_relations.ma constructive_connectives.ma higher_order_defs/relations.ma
18 infsup.ma sandwich_corollary.ma
19 constructive_pointfree/lebesgue.ma constructive_connectives.ma metric_lattice.ma sequence.ma
20 classical_pointwise/topology.ma classical_pointwise/sets.ma
21 classical_pointwise/sigma_algebra.ma classical_pointwise/topology.ma
22 classical_pointwise/sets.ma logic/connectives.ma nat/nat.ma
23 classical_pointfree/ordered_sets.ma excess.ma
24 classical_pointfree/ordered_sets2.ma classical_pointfree/ordered_sets.ma
25 attic/fields.ma attic/rings.ma
26 attic/reals.ma attic/ordered_fields_ch0.ma
27 attic/integration_algebras.ma attic/vector_spaces.ma lattice.ma
28 attic/vector_spaces.ma attic/reals.ma
29 attic/rings.ma group.ma
30 attic/ordered_fields_ch0.ma group.ma attic/fields.ma ordered_group.ma
31 Q/q.ma 
32 higher_order_defs/relations.ma 
33 logic/connectives.ma 
34 nat/nat.ma 
35 nat/orders.ma 
36 nat/plus.ma 
37 nat/times.ma