OAI/Geometry/Cannon/PlaneTopology/Plane.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CannonRegularDisk.Plane line 16
2. abbrev OAI.CannonRegularDisk.RoundSphere line 17
3. def OAI.CannonRegularDisk.IsRegularDisk line 22
4. lemma OAI.CannonRegularDisk.IsRegularDisk.isOpen line 26
5. lemma OAI.CannonRegularDisk.IsRegularDisk.image line 30
6. lemma OAI.CannonRegularDisk.IsRegularDisk.preimage line 35
7. theorem OAI.CannonRegularDisk.IsRegularDisk.closed_certificate line 44
8. lemma OAI.CannonRegularDisk.small_regular_disk line 64
9. theorem OAI.CannonRegularDisk.uniform_regular_disk_neighborhoods line 93