OAI/Geometry/CylinderCovering/Angular/OrdinaryCapsDefinitions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CylinderCovering.AngularOrdinaryCaps.secantAlpha line 11
2. def OAI.CylinderCovering.AngularOrdinaryCaps.secantBeta line 12
3. def OAI.CylinderCovering.AngularOrdinaryCaps.taggedRadius line 14
4. def OAI.CylinderCovering.AngularOrdinaryCaps.midpointRadius line 15
5. def OAI.CylinderCovering.AngularOrdinaryCaps.maximumRadius line 16
6. def OAI.CylinderCovering.AngularOrdinaryCaps.radialRadius line 18
7. inductive OAI.CylinderCovering.AngularOrdinaryCaps.CapChoice line 20
8. def OAI.CylinderCovering.AngularOrdinaryCaps.chosenRadius line 26
9. def OAI.CylinderCovering.AngularOrdinaryCaps.ordinaryData line 32
10. def OAI.CylinderCovering.AngularOrdinaryCaps.OrdinaryCoverStatement line 40