OAI/Geometry/Borsuk/MatrixGeometry/FinitePositiveBound.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.BorsukNine.finite_positive_boundline 13 - lemma
OAI.BorsukNine.SimplicialChains.odd_homotopy_local_modelsline 27