OAI/Topology/ArtinGroups/Realizations/WeightInsertRetract.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.weightInsertRetract line 12
2. lemma OAI.HarmonicArtin.weightInsertRetract_old line 20
3. def OAI.HarmonicArtin.WeightRetractionPiece.initial line 36
4. lemma OAI.HarmonicArtin.WeightRetractionPiece.missing_minimal line 46
5. theorem OAI.HarmonicArtin.WeightRetractionPiece.insertLinkContractible line 66
6. def OAI.HarmonicArtin.WeightRetractionPiece.successor line 70
7. lemma OAI.HarmonicArtin.WeightRetractionPiece.extends_successor line 89
8. theorem OAI.HarmonicArtin.orderWeights_retract_of_initial line 98
9. theorem OAI.HarmonicArtin.orderWeights_retract_of_lower_fibers line 128
10. lemma OAI.HarmonicArtin.contractible_of_continuous_retract line 160