OAI/Geometry/Borsuk/SphereGeometry/SphereMeasure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BorsukNine.UnitSphere line 14
2. def OAI.BorsukNine.sphereProbability line 16
3. instance OAI.BorsukNine.sphereMeasure_neZero line 19
4. instance OAI.BorsukNine.sphereProbability_isProbability line 24
5. instance OAI.BorsukNine.sphereProbability_openPos line 28
6. def OAI.BorsukNine.sphereRotation line 34
7. lemma OAI.BorsukNine.sphereRotation_preserves_toSphere line 38
8. lemma OAI.BorsukNine.sphereRotation_preserves_probability line 66
9. lemma OAI.BorsukNine.integral_sphere_rotation line 71