OAI/Geometry/SingularHomology/FiniteSimplicialHomology.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem340.finiteDimensional_shortComplex_homology line 11
  2. theorem OAI.Problem340.finiteDimensional_normalized_real_chains line 19
  3. theorem OAI.Problem340.finiteDimensional_real_simplicial_homology line 30
  4. theorem OAI.Problem340.real_simplicial_homology_finite_support line 41
  5. theorem OAI.Problem340.bddAbove_real_simplicial_eigenpair_moduli line 49
  6. theorem OAI.Problem340.finrank_shortComplex_homology_le line 62
  7. theorem OAI.Problem340.finrank_normalized_real_chains line 70
  8. theorem OAI.Problem340.finrank_real_simplicial_homology_le line 86