OAI/Topology/ArtinGroups/Realizations/OrderWeights.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HarmonicArtin.OrderWeights line 13
2. lemma OAI.HarmonicArtin.OrderWeights.ext line 19
3. lemma OAI.HarmonicArtin.OrderWeights.support_nonempty line 22
4. def OAI.HarmonicArtin.chainWeights line 29
5. lemma OAI.HarmonicArtin.chainWeights_apply line 32
6. lemma OAI.HarmonicArtin.chainWeights_nonneg line 36
7. lemma OAI.HarmonicArtin.chainWeights_total line 41
8. lemma OAI.HarmonicArtin.chainWeights_support line 46
9. def OAI.HarmonicArtin.orderWeightsOfChain line 54
10. def OAI.HarmonicArtin.nerveChain line 64
11. def OAI.HarmonicArtin.orderWeightsChart line 68
12. instance OAI.HarmonicArtin.(instance at line 71) line 71
13. lemma OAI.HarmonicArtin.orderWeightsChart_continuous line 75
14. lemma OAI.HarmonicArtin.orderWeights_continuous_iff line 81
15. lemma OAI.HarmonicArtin.chainWeights_natural line 93