OAI/Topology/ArtinGroups/Realizations/WeightAffineValue.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.weightAffineValue line 13
2. lemma OAI.HarmonicArtin.weightAffineValue_sum line 16
3. lemma OAI.HarmonicArtin.weightAffineValue_fintype line 19
4. lemma OAI.HarmonicArtin.OrderWeights.total_fintype line 23
5. lemma OAI.HarmonicArtin.weightAffineValue_vertex line 27
6. lemma OAI.HarmonicArtin.weightAffineValue_delete line 30
7. lemma OAI.HarmonicArtin.weightAffineValue_continuous line 39
8. lemma OAI.HarmonicArtin.weightAffineValue_mem line 44
9. lemma OAI.HarmonicArtin.weightAffineValue_map line 49
10. lemma OAI.HarmonicArtin.weightAffineValue_le line 54
11. lemma OAI.HarmonicArtin.weightAffineValue_eq_iff line 62
12. def OAI.HarmonicArtin.weightMax line 77
13. lemma OAI.HarmonicArtin.weightMax_mem line 79
14. lemma OAI.HarmonicArtin.le_weightMax line 82
15. lemma OAI.HarmonicArtin.weightAffineValue_cone line 88