OAI/Geometry/CAT0Fillings/Model.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CAT0Fillings.Euc line 14

   Also declared: ComparatorChallenges/SharpCAT0Filling.lean:14 (same declaration text).

2. abbrev OAI.CAT0Fillings.Functional line 15

   Also declared: ComparatorChallenges/SharpCAT0Filling.lean:15 (same declaration text).

3. def OAI.CAT0Fillings.BoundedLip line 21

   Also declared: ComparatorChallenges/SharpCAT0Filling.lean:21 (same declaration text).

4. def OAI.CAT0Fillings.Admissible line 24

   Also declared: ComparatorChallenges/SharpCAT0Filling.lean:24 (same declaration text).

5. def OAI.CAT0Fillings.Controls line 27

   Also declared: ComparatorChallenges/SharpCAT0Filling.lean:27 (same declaration text).

6. def OAI.CAT0Fillings.mass line 32

   Also declared: ComparatorChallenges/SharpCAT0Filling.lean:32 (same declaration text).

7. structure OAI.CAT0Fillings.IsMetricCurrent line 36

   Also declared: ComparatorChallenges/SharpCAT0Filling.lean:36 (same declaration text).

8. def OAI.CAT0Fillings.boundarySucc line 54

   Also declared: ComparatorChallenges/SharpCAT0Filling.lean:54 (same declaration text).

9. def OAI.CAT0Fillings.boundary line 57

   Also declared: ComparatorChallenges/SharpCAT0Filling.lean:57 (same declaration text).

10. structure OAI.CAT0Fillings.IntegerChart line 61

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:61 (same declaration text).

11. def OAI.CAT0Fillings.IntegerChart.scalar line 74

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:74 (same declaration text).

12. def OAI.CAT0Fillings.IntegerChart.jacobian line 77

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:77 (same declaration text).

13. def OAI.CAT0Fillings.IntegerChart.action line 81

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:81 (same declaration text).

14. def OAI.CAT0Fillings.IntegerChart.image line 86

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:86 (same declaration text).

15. def OAI.CAT0Fillings.IntegerRectifiable line 90

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:90 (same declaration text).

16. def OAI.CAT0Fillings.IsIntegral line 97

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:97 (same declaration text).

17. abbrev OAI.CAT0Fillings.IntegralCurrent line 102

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:102 (same declaration text).

18. def OAI.CAT0Fillings.CompactlySupported line 105

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:105 (same declaration text).

19. def OAI.CAT0Fillings.IsCycle line 109

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:109 (same declaration text).

20. def OAI.CAT0Fillings.IsCAT0 line 116

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:116 (same declaration text).

21. def OAI.CAT0Fillings.omega line 128

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:128 (same declaration text).

22. def OAI.CAT0Fillings.sphereArea line 130

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:130 (same declaration text).

23. def OAI.CAT0Fillings.fillingCoefficient line 131

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:131 (same declaration text).

24. def OAI.CAT0Fillings.fillingPower line 133

    Also declared: ComparatorChallenges/SharpCAT0Filling.lean:133 (same declaration text).