OAI/Geometry/SingularHomology/SingularCoverNaturalityExtended.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem340.SingularCover.restrict line 14
2. theorem OAI.Problem340.SingularCover.restrict_ι line 18
3. theorem OAI.Problem340.SingularCover.inf_le_preimage line 22
4. theorem OAI.Problem340.SingularCover.sup_le_preimage line 27
5. abbrev OAI.Problem340.SingularCover.chainsFunctor line 32
6. theorem OAI.Problem340.SingularCover.connecting_naturality line 35
7. theorem OAI.Problem340.SingularCover.connecting_naturality_apply line 51
8. theorem OAI.Problem340.SingularCover.supported_le_preimage_of_mapsTo line 69
9. def OAI.Problem340.SingularCover.continuousUnionShortComplexMap line 77