OAI/Geometry/PeriodicTiling/PeriodicVolumeOrbits.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PeriodicTilingThree.PeriodicVolume.representatives line 15
2. theorem OAI.PeriodicTilingThree.PeriodicVolume.representatives_finite line 18
3. def OAI.PeriodicTilingThree.PeriodicVolume.orbitMap line 23
4. theorem OAI.PeriodicTilingThree.PeriodicVolume.orbitMap_injective line 29
5. theorem OAI.PeriodicTilingThree.PeriodicVolume.orbitMap_surjective line 48
6. def OAI.PeriodicTilingThree.PeriodicVolume.orbitEquiv line 64
7. theorem OAI.PeriodicTilingThree.PeriodicVolume.orbitEquiv_apply_coe line 70
8. theorem OAI.PeriodicTilingThree.PeriodicVolume.type_constant_on_orbit line 76