OAI/Topology/ArtinGroups/Realizations/WeightRetractionPiece.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HarmonicArtin.WeightRetractionPiece line 12
2. def OAI.HarmonicArtin.WeightRetractionPiece.Extends line 22
3. lemma OAI.HarmonicArtin.WeightRetractionPiece.extends_refl line 26
4. lemma OAI.HarmonicArtin.WeightRetractionPiece.extends_trans line 31
5. instance OAI.HarmonicArtin.WeightRetractionPiece.(instance at line 38) line 38
6. lemma OAI.HarmonicArtin.WeightRetractionPiece.extends_compare line 40
7. def OAI.HarmonicArtin.WeightRetractionPiece.unionCarrier line 53
8. lemma OAI.HarmonicArtin.WeightRetractionPiece.subset_union line 54
9. lemma OAI.HarmonicArtin.WeightRetractionPiece.union_finset_cover line 58
10. def OAI.HarmonicArtin.WeightRetractionPiece.unionIncl line 77
11. lemma OAI.HarmonicArtin.WeightRetractionPiece.union_map_cover line 81
12. def OAI.HarmonicArtin.WeightRetractionPiece.unionLocal line 92
13. lemma OAI.HarmonicArtin.WeightRetractionPiece.union_compatible line 96
14. def OAI.HarmonicArtin.WeightRetractionPiece.unionMap line 106
15. lemma OAI.HarmonicArtin.WeightRetractionPiece.unionMap_on line 110
16. def OAI.HarmonicArtin.WeightRetractionPiece.union line 114
17. lemma OAI.HarmonicArtin.WeightRetractionPiece.extends_union line 132