OAI/Geometry/Borsuk/SphereGeometry/NormSphere.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.BorsukNine.normSphereline 10 - lemma
OAI.BorsukNine.sphere_null_local_modelsline 15
OAI/Geometry/Borsuk/SphereGeometry/NormSphere.lean2 declarations, 0 contain sorry, 0 declared as axioms
OAI.BorsukNine.normSphere line 10OAI.BorsukNine.sphere_null_local_models line 15