OAI/Topology/ArtinGroups/Harmonic/Initial.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.weight_eq_vertex_subsingleton line 14
2. def OAI.HarmonicArtin.WeightContractionPiece.initial line 27
3. lemma OAI.HarmonicArtin.WeightContractionPiece.missing_minimal line 43
4. def OAI.HarmonicArtin.WeightContractionPiece.insertLinkContractionPoint line 62
5. def OAI.HarmonicArtin.WeightContractionPiece.insertLinkContraction line 66
6. def OAI.HarmonicArtin.WeightContractionPiece.successor line 73
7. lemma OAI.HarmonicArtin.WeightContractionPiece.extends_successor line 91
8. theorem OAI.HarmonicArtin.orderWeights_contractible_of_earlier_links line 104