OAI/Geometry/SingularHomology/HomologySpectrumFactor.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem340.homology_pairRadii_factor_subsetline 15 - theorem
OAI.Problem340.bddAbove_homology_pairRadii_of_homotopy_factorline 26 - theorem
OAI.Problem340.bddAbove_homology_pairRadii_of_finite_homotopy_factorline 40 - theorem
OAI.Problem340.totalRealHomologySpectralRadius_eq_sSup_pairRadiiline 53