OAI/Geometry/WeakMTW/Model.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.WeakMTWGlobalSupport.WeakMTW.Model line 16

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

2. abbrev OAI.WeakMTWGlobalSupport.WeakMTW.model line 17

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

3. def OAI.WeakMTWGlobalSupport.WeakMTW.CompleteGeodesicWithInitialData line 26

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

4. def OAI.WeakMTWGlobalSupport.WeakMTW.ExpEndpoint line 35

   Also declared: ComparatorChallenges/WeakMTWGlobalSupport.lean:33 (same declaration text).

5. def OAI.WeakMTWGlobalSupport.WeakMTW.exp line 38

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

6. def OAI.WeakMTWGlobalSupport.WeakMTW.injectivityDomain line 43

   Also declared: ComparatorChallenges/WeakMTWGlobalSupport.lean:41 (same declaration text).

7. def OAI.WeakMTWGlobalSupport.WeakMTW.cost line 46

   Also declared: ComparatorChallenges/WeakMTWGlobalSupport.lean:44 (same declaration text).

8. def OAI.WeakMTWGlobalSupport.WeakMTW.mtw line 48

   Also declared: ComparatorChallenges/WeakMTWGlobalSupport.lean:46 (same declaration text).

9. def OAI.WeakMTWGlobalSupport.WeakMTW.HasWeakMTW line 53

   Also declared: ComparatorChallenges/WeakMTWGlobalSupport.lean:51 (same declaration text).

10. def OAI.WeakMTWGlobalSupport.WeakMTW.MainConvexity line 57

    Also declared: ComparatorChallenges/WeakMTWGlobalSupport.lean:55 (same declaration text).