OAI/Geometry/Borsuk/LocalParity/Sard.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.BorsukNine.exists_regular_valueline 10 - lemma
OAI.BorsukNine.compact_regular_level_finiteline 29
OAI/Geometry/Borsuk/LocalParity/Sard.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.BorsukNine.exists_regular_value line 10OAI.BorsukNine.compact_regular_level_finite line 29