OAI/Geometry/CylinderCovering/Angular/PartitionIdentities.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AngularPartitionIdentities.node_zero line 7
2. lemma OAI.AngularPartitionIdentities.node_last line 9
3. lemma OAI.AngularPartitionIdentities.node_step line 15
4. lemma OAI.AngularPartitionIdentities.node_strict line 21
5. lemma OAI.AngularPartitionIdentities.node_bounds line 28
6. lemma OAI.AngularPartitionIdentities.node_abs_le line 39
7. lemma OAI.AngularPartitionIdentities.node_width_le line 43
8. theorem OAI.AngularPartitionIdentities.partition_properties line 50