OAI/Geometry/TranslativeCovering/SphericalLaw.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SphericalLaw.Space line 13
2. abbrev OAI.SphericalLaw.Sphere line 14
3. def OAI.SphericalLaw.σ line 16
4. instance OAI.SphericalLaw.probability line 19
5. lemma OAI.SphericalLaw.sphere_singleton_zero line 25
6. instance OAI.SphericalLaw.nonatomic line 48
7. def OAI.SphericalLaw.act line 53
8. lemma OAI.SphericalLaw.continuous_act line 56
9. lemma OAI.SphericalLaw.cone_preimage line 59
10. lemma OAI.SphericalLaw.invariant line 79
11. def OAI.SphericalLaw.cap line 91
12. lemma OAI.SphericalLaw.cap_open line 94
13. lemma OAI.SphericalLaw.cap_measurable line 97
14. lemma OAI.SphericalLaw.positive_open line 100
15. lemma OAI.SphericalLaw.cap_positive line 107
16. lemma OAI.SphericalLaw.cap_equal_norm line 114
17. lemma OAI.SphericalLaw.cap_smul line 125
18. lemma OAI.SphericalLaw.cutting_mass_le line 132