OAI/Geometry/CylinderCovering/Simplex/Diameter.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.SimplexDiameter.chordLength_zero line 11
2. lemma OAI.CylinderCovering.SimplexDiameter.chordLength_le_diam line 16
3. lemma OAI.CylinderCovering.SimplexDiameter.chordLength_segment line 23
4. lemma OAI.CylinderCovering.SimplexDiameter.chordLengths_compact line 29
5. lemma OAI.CylinderCovering.SimplexDiameter.maxChord_attained line 48
6. lemma OAI.CylinderCovering.SimplexDiameter.maxChord_nonneg line 52
7. lemma OAI.CylinderCovering.SimplexDiameter.maxChord_le_diam line 56
8. lemma OAI.CylinderCovering.SimplexDiameter.chordLength_le_maxChord line 60
9. lemma OAI.CylinderCovering.SimplexDiameter.compact_diameter_attained line 66
10. lemma OAI.CylinderCovering.SimplexDiameter.exists_maxChord_eq_diam line 76
11. lemma OAI.CylinderCovering.SimplexDiameter.convexHull_pair_distance line 91
12. lemma OAI.CylinderCovering.SimplexDiameter.finite_convexHull_diameter_attained line 98
13. lemma OAI.CylinderCovering.SimplexDiameter.regular_convexHull_diameter line 105
14. lemma OAI.CylinderCovering.SimplexDiameter.maxChord_pos_of_interior line 121
15. lemma OAI.CylinderCovering.SimplexDiameter.projection_minimum_of_chord_identity line 134
16. lemma OAI.CylinderCovering.SimplexDiameter.finite_edge_maxChord line 149
17. lemma OAI.CylinderCovering.SimplexDiameter.finite_edge_projection_minimizer line 174
18. lemma OAI.CylinderCovering.SimplexDiameter.affineIndependent_diameter_pos line 195
19. lemma OAI.CylinderCovering.SimplexDiameter.regular_edge_maxChord line 204