OAI/Geometry/SingularHomology/SimplicialMayerVietoris.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem340.SimplicialMayerVietoris.coefficients line 11
2. abbrev OAI.Problem340.SimplicialMayerVietoris.sequence line 15
3. def OAI.Problem340.SimplicialMayerVietoris.connecting line 17
4. theorem OAI.Problem340.SimplicialMayerVietoris.middle_homology_isZero line 22
5. theorem OAI.Problem340.SimplicialMayerVietoris.connecting_injective line 33
6. theorem OAI.Problem340.SimplicialMayerVietoris.connecting_range line 41
7. theorem OAI.Problem340.SimplicialMayerVietoris.connecting_kernel line 46
8. def OAI.Problem340.SimplicialMayerVietoris.connectingIso line 51