OAI/Topology/ArtinGroups/Harmonic/UnionCarrier.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.HarmonicArtin.WeightContractionPiece.(instance at line 15) line 15
2. def OAI.HarmonicArtin.WeightContractionPiece.unionCarrier line 19
3. lemma OAI.HarmonicArtin.WeightContractionPiece.subset_union line 20
4. lemma OAI.HarmonicArtin.WeightContractionPiece.union_finset_cover line 24
5. def OAI.HarmonicArtin.WeightContractionPiece.unionIncl line 43
6. lemma OAI.HarmonicArtin.WeightContractionPiece.unionIncl_ambient line 46
7. lemma OAI.HarmonicArtin.WeightContractionPiece.union_map_cover line 49
8. def OAI.HarmonicArtin.WeightContractionPiece.unionLocal line 60
9. lemma OAI.HarmonicArtin.WeightContractionPiece.union_compatible line 64
10. def OAI.HarmonicArtin.WeightContractionPiece.unionMap line 77
11. lemma OAI.HarmonicArtin.WeightContractionPiece.unionMap_on line 80
12. def OAI.HarmonicArtin.WeightContractionPiece.union line 84
13. lemma OAI.HarmonicArtin.WeightContractionPiece.extends_union line 106