OAI/Topology/ArtinGroups/Realizations/WeightOld.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.WeightOld line 14
2. abbrev OAI.HarmonicArtin.WeightLink line 15
3. abbrev OAI.HarmonicArtin.weightOldIncl line 16
4. abbrev OAI.HarmonicArtin.weightLinkIncl line 17
5. abbrev OAI.HarmonicArtin.weightLinkOld line 18
6. def OAI.HarmonicArtin.weightOldMap line 19
7. def OAI.HarmonicArtin.weightLinkMap line 21
8. def OAI.HarmonicArtin.weightConeMap line 23
9. lemma OAI.HarmonicArtin.weightMap_zero_of_not_range line 26
10. lemma OAI.HarmonicArtin.weightOldMap_at line 33
11. lemma OAI.HarmonicArtin.weightConeMap_at line 38
12. lemma OAI.HarmonicArtin.weightConeMap_zero line 48
13. lemma OAI.HarmonicArtin.weightConeMap_one line 54
14. lemma OAI.HarmonicArtin.weightConeMap_eq_cone line 57
15. lemma OAI.HarmonicArtin.weightOld_surjective_zero line 78
16. lemma OAI.HarmonicArtin.weightDelete_link line 85
17. lemma OAI.HarmonicArtin.weightDelete_reconstruct line 91
18. lemma OAI.HarmonicArtin.weightParts_surjective line 108