OAI/Geometry/SingularHomology/SmallCoverMayerVietoris.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.simplicialMayerVietoris_sequence_eq_unionShortComplex line 12
  2. def OAI.Problem340.SmallCoverMayerVietoris.binaryCover line 22
  3. theorem OAI.Problem340.SmallCoverMayerVietoris.small_binaryCover line 24
  4. def OAI.Problem340.SmallCoverMayerVietoris.smallUnionHomologyIso line 28
  5. def OAI.Problem340.SmallCoverMayerVietoris.intersectionHomologyIso line 35
  6. def OAI.Problem340.SmallCoverMayerVietoris.connecting line 43
  7. theorem OAI.Problem340.SmallCoverMayerVietoris.member_homology_isZero line 50
  8. theorem OAI.Problem340.SmallCoverMayerVietoris.connecting_injective line 55
  9. def OAI.Problem340.SmallCoverMayerVietoris.connectingIso line 64
  10. theorem OAI.Problem340.SmallCoverMayerVietoris.connectingIso_hom line 74
  11. def OAI.Problem340.SmallCoverMayerVietoris.singularConnectingIsoOfQuasiIsoAt line 78
  12. theorem OAI.Problem340.SmallCoverMayerVietoris.inclusion_singularConnectingIsoOfQuasiIsoAt line 85