OAI/Geometry/CylinderCovering/Nilpotent/Finite.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.Nilpotent.height_continuous line 14
  2. lemma OAI.CylinderCovering.Nilpotent.height_le_uniform line 18
  3. lemma OAI.CylinderCovering.Nilpotent.truncatedLabels_isCompact line 25
  4. lemma OAI.CylinderCovering.Nilpotent.truncatedLabels_upper line 48
  5. lemma OAI.CylinderCovering.Nilpotent.angularField_contDiffOn line 53
  6. lemma OAI.CylinderCovering.Nilpotent.angularField_smoothNear line 68
  7. lemma OAI.CylinderCovering.Nilpotent.angularField_radial line 74
  8. lemma OAI.CylinderCovering.Nilpotent.signedSweep_subset_apex_union line 78
  9. lemma OAI.CylinderCovering.Nilpotent.angularField_square_zero line 92
  10. lemma OAI.CylinderCovering.Nilpotent.truncated_physical_cover line 100
  11. lemma OAI.CylinderCovering.Nilpotent.physical_second_cover line 114
  12. lemma OAI.CylinderCovering.Nilpotent.lowerSweep_mem_signed line 129
  13. lemma OAI.CylinderCovering.Nilpotent.upperSweep_mem_signed line 136
  14. lemma OAI.CylinderCovering.Nilpotent.tetrahedron_subset_signed_sweeps line 143
  15. lemma OAI.CylinderCovering.Nilpotent.complete_signed_cover_of_estimates line 157
  16. lemma OAI.CylinderCovering.Nilpotent.finite_counterexample_of_signed_covers line 173
  17. lemma OAI.CylinderCovering.Nilpotent.exists_padding_and_collar line 190