OAI/Geometry/CylinderCovering/Nilpotent/Counterexample.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.Nilpotent.complete_signed_cover line 13
2. theorem OAI.CylinderCovering.Nilpotent.finite_counterexample_at_parameter line 25
3. theorem OAI.CylinderCovering.Nilpotent.finite_counterexample line 50
4. lemma OAI.CylinderCovering.Nilpotent.relativeCost_le_normalized_area line 57
5. theorem OAI.CylinderCovering.Nilpotent.normalized_finite_counterexample line 68