OAI/Dynamics/EntropyCounterexample/SmallCoverNaturality.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.SmallCoverMayerVietoris.eqToHom_subcomplex_inclusion line 18
  2. theorem OAI.Problem340.SmallCoverMayerVietoris.restrictedMap_eqToHom line 23
  3. abbrev OAI.Problem340.SmallCoverMayerVietoris.singularMap line 36
  4. theorem OAI.Problem340.SmallCoverMayerVietoris.inSubset_le_preimage line 39
  5. theorem OAI.Problem340.SmallCoverMayerVietoris.binary_le_preimage line 45
  6. def OAI.Problem340.SmallCoverMayerVietoris.binaryMap line 53
  7. theorem OAI.Problem340.SmallCoverMayerVietoris.binaryMap_inclusion line 59
  8. theorem OAI.Problem340.SmallCoverMayerVietoris.binaryHomologyMap_inclusion line 65
  9. theorem OAI.Problem340.SmallCoverMayerVietoris.smallUnionHomologyIso_naturality line 78
  10. def OAI.Problem340.SmallCoverMayerVietoris.intersectionMap line 99
  11. theorem OAI.Problem340.SmallCoverMayerVietoris.restrictedMap_inSubset line 104
  12. theorem OAI.Problem340.SmallCoverMayerVietoris.subspaceHomologyIso_naturality line 109
  13. theorem OAI.Problem340.SmallCoverMayerVietoris.intersectionHomologyIso_naturality line 120
  14. theorem OAI.Problem340.SmallCoverMayerVietoris.transport_connecting_naturality line 157
  15. theorem OAI.Problem340.SmallCoverMayerVietoris.connecting_naturality line 171
  16. theorem OAI.Problem340.SmallCoverMayerVietoris.descend_connecting_naturality line 199
  17. theorem OAI.Problem340.SmallCoverMayerVietoris.singularConnectingIsoOfQuasiIsoAt_naturality line 209
  18. theorem OAI.Problem340.SmallCoverMayerVietoris.singularConnectingIsoOfQuasiIsoAt_naturality_apply line 232