OAI/Probability/ClassicalON/TorusDouble.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ClassicalON.PlanarAngle line 11
2. def OAI.ClassicalON.angleLaw line 13
3. instance OAI.ClassicalON.angleLaw_isProbability line 15
4. instance OAI.ClassicalON.angleLaw_isAddHaar line 17
5. def OAI.ClassicalON.planarReference line 22
6. instance OAI.ClassicalON.planarReference_isProbability line 24
7. instance OAI.ClassicalON.planarReference_isAddHaar line 26
8. def OAI.ClassicalON.torusDouble line 29
9. theorem OAI.ClassicalON.torusDouble_continuous line 36
10. theorem OAI.ClassicalON.torusDouble_surjective line 41
11. theorem OAI.ClassicalON.torusDouble_preserves line 52