OAI/Geometry/CylinderCovering/Barycentric/Finite.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RadialCoordinates.BarycentricFinite.firstBase_transport line 16
2. lemma OAI.RadialCoordinates.BarycentricFinite.secondBase_transport line 33
3. lemma OAI.RadialCoordinates.BarycentricFinite.firstAxis_sum line 50
4. lemma OAI.RadialCoordinates.BarycentricFinite.secondAxis_sum line 54
5. lemma OAI.RadialCoordinates.BarycentricFinite.projection_sum line 58
6. lemma OAI.RadialCoordinates.BarycentricFinite.projection_perpendicular line 63
7. lemma OAI.RadialCoordinates.BarycentricFinite.mem_projection_cylinder line 68
8. lemma OAI.RadialCoordinates.BarycentricFinite.scaled_base_compact line 74
9. lemma OAI.RadialCoordinates.BarycentricFinite.firstBase_sum line 82
10. lemma OAI.RadialCoordinates.BarycentricFinite.secondBase_sum line 87
11. lemma OAI.RadialCoordinates.BarycentricFinite.finite_cover line 92
12. lemma OAI.RadialCoordinates.BarycentricFinite.two_J_eq_scaled_physicalCost line 116
13. lemma OAI.RadialCoordinates.BarycentricFinite.totalArea_nonneg line 122
14. lemma OAI.RadialCoordinates.BarycentricFinite.totalArea_eventually_le line 127
15. lemma OAI.RadialCoordinates.BarycentricFinite.totalArea_limsup_le line 139
16. lemma OAI.RadialCoordinates.BarycentricFinite.base_properties line 146
17. theorem OAI.RadialCoordinates.BarycentricFinite.finite_barycentric_sweeps line 192