OAI/Geometry/CylinderCovering/Nilpotent/DomainExample.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RuledApproximation.NilpotentDomainExample.field_apply line 12
2. lemma OAI.RuledApproximation.NilpotentDomainExample.field_contDiff line 16
3. lemma OAI.RuledApproximation.NilpotentDomainExample.field_fderiv_apply line 20
4. lemma OAI.RuledApproximation.NilpotentDomainExample.field_squareZero_iff line 30
5. lemma OAI.RuledApproximation.NilpotentDomainExample.labels_compact line 43
6. lemma OAI.RuledApproximation.NilpotentDomainExample.zero_mem_labels line 52
7. lemma OAI.RuledApproximation.NilpotentDomainExample.labels_volume_zero line 57
8. lemma OAI.RuledApproximation.NilpotentDomainExample.field_squareZero_on_labels line 74
9. lemma OAI.RuledApproximation.NilpotentDomainExample.no_squareZero_neighborhood line 79
10. lemma OAI.RuledApproximation.NilpotentDomainExample.field_smoothNear line 95
11. theorem OAI.RuledApproximation.NilpotentDomainExample.physical_cover line 98
12. theorem OAI.RuledApproximation.NilpotentDomainExample.physical_pair line 104