OAI/Geometry/CylinderCovering/Barycentric/Closure.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CylinderCovering.BarycentricClosure.closure_positive_simplex line 13
2. theorem OAI.CylinderCovering.BarycentricClosure.simplex_subset_of_positive_subset line 47
3. theorem OAI.CylinderCovering.BarycentricClosure.simplex_subset_compact_union line 54
4. theorem OAI.CylinderCovering.BarycentricClosure.barycentricSimplex_subset_of_positive_subset line 60
5. theorem OAI.RadialCoordinates.mem_firstSweepWithCap_iff line 76
6. theorem OAI.RadialCoordinates.mem_secondSweepWithCap_iff line 85
7. theorem OAI.RadialCoordinates.firstSweepPoint_sum line 94
8. theorem OAI.RadialCoordinates.secondSweepPoint_sum line 98
9. theorem OAI.RadialCoordinates.firstSweepPoint_coordinates line 102
10. theorem OAI.RadialCoordinates.secondSweepPoint_coordinates line 111
11. theorem OAI.RadialCoordinates.continuous_firstSweepPoint line 120
12. theorem OAI.RadialCoordinates.continuous_secondSweepPoint line 125
13. theorem OAI.RadialCoordinates.isCompact_firstSweepWithCap line 130
14. theorem OAI.RadialCoordinates.isCompact_secondSweepWithCap line 136
15. theorem OAI.RadialCoordinates.continuous_barycentric_cap line 142
16. theorem OAI.RadialCoordinates.barycentric_cap_nonneg line 146
17. theorem OAI.RadialCoordinates.isCompact_firstSweep line 150
18. theorem OAI.RadialCoordinates.isCompact_secondSweep line 153
19. theorem OAI.RadialCoordinates.barycentric_cover_of_positive_cover line 156