OAI/Geometry/SingularHomology/SingularSmallChainSupport.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.simplicialChainMap_finsupp line 12
  2. theorem OAI.Problem340.finsupp_range_lmapDomain_eq_supported line 28
  3. theorem OAI.Problem340.mem_range_simplicialChainMap_iff line 34
  4. theorem OAI.Problem340.mem_range_subcomplex_chainMap_iff line 49
  5. theorem OAI.Problem340.finsupp_domLCongr_mem_supported_iff line 58
  6. theorem OAI.Problem340.mem_range_singularSubcomplex_iff line 72
  7. theorem OAI.Problem340.SingularSmallChains.mem_range_inclusion_iff_supported line 88
  8. theorem OAI.Problem340.SingularSmallChains.mem_range_inclusion_iff_support line 98
  9. theorem OAI.Problem340.SingularSmallChains.exists_chain_of_finsupp_support line 107
  10. abbrev OAI.Problem340.SingularSmallChains.supportedChains line 115
  11. def OAI.Problem340.SingularSmallChains.toSupportedChains line 120
  12. def OAI.Problem340.SingularSmallChains.chainsEquivSupported line 126
  13. theorem OAI.Problem340.SingularSmallChains.chainsEquivSupported_apply_val line 145
  14. theorem OAI.Problem340.SingularSmallChains.inclusion_chainsEquivSupported_symm line 151