OAI/Topology/ArtinGroups/Harmonic/ProductBoxSlice.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.weight_contractible_of_order_retraction line 13
2. abbrev OAI.HarmonicArtin.ProductBoxSlice line 22
3. def OAI.HarmonicArtin.productBoxProject line 24
4. def OAI.HarmonicArtin.productBoxSection line 29
5. lemma OAI.HarmonicArtin.productBox_contractible line 44
6. abbrev OAI.HarmonicArtin.ProductBoundary line 56
7. def OAI.HarmonicArtin.productBoundarySliceIso line 58
8. def OAI.HarmonicArtin.productBoundaryFiberIso line 66
9. theorem OAI.HarmonicArtin.productBoundary_contractible line 77