OAI/Geometry/Borsuk/Support/MixedHits.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.BorsukNine.Admissible.mixedHomotopy_hitline 16 - lemma
OAI.BorsukNine.Admissible.negative_trace_posline 44 - lemma
OAI.BorsukNine.Admissible.original_ray_levelline 52