OAI/Geometry/SingularHomology/SingularSupportNaturality.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.singularCover_supported_eq_inSubset line 12
2. theorem OAI.Problem340.SingularSmallChains.subspaceIso_hom_inclusion line 20
3. def OAI.Problem340.SingularSmallChains.restrictMap line 26
4. def OAI.Problem340.SingularSmallChains.mapInSubset line 31
5. theorem OAI.Problem340.SingularSmallChains.subspaceIso_naturality line 42
6. theorem OAI.Problem340.SingularSmallChains.mapInSubset_inclusion line 50
7. theorem OAI.Problem340.SingularSmallChains.subspaceHomologyIso_inclusion_apply line 57
8. theorem OAI.Problem340.SingularSmallChains.subspaceHomologyIso_naturality_apply line 68