OAI/Dynamics/EntropyCounterexample/Definitions.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem340.ClockAmbient line 11

   Also declared: ComparatorChallenges/C1EntropyCounterexample.lean:11 (same declaration text).

2. abbrev OAI.Problem340.SphereAmbient line 13

   Also declared: ComparatorChallenges/C1EntropyCounterexample.lean:13 (same declaration text).

3. abbrev OAI.Problem340.StandardClock line 15

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

4. abbrev OAI.Problem340.StandardSphere2 line 17

   Also declared: ComparatorChallenges/C1EntropyCounterexample.lean:17 (same declaration text).

5. abbrev OAI.Problem340.CounterexampleManifold line 19

   Also declared: ComparatorChallenges/C1EntropyCounterexample.lean:19 (same declaration text).

6. abbrev OAI.Problem340.CounterexampleAmbient line 22

   Also declared: ComparatorChallenges/C1EntropyCounterexample.lean:22 (same declaration text).

7. def OAI.Problem340.standardEmbedding line 25

   Also declared: ComparatorChallenges/C1EntropyCounterexample.lean:25 (same declaration text).

8. def OAI.Problem340.IsC1SelfMap line 29

   Also declared: ComparatorChallenges/C1EntropyCounterexample.lean:29 (same declaration text).

9. def OAI.Problem340.continuousMapOf line 40

   Also declared: ComparatorChallenges/C1EntropyCounterexample.lean:40 (same declaration text).

10. abbrev OAI.Problem340.RealSingularHomology line 44

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

11. def OAI.Problem340.realHomologyMap line 48

    Also declared: ComparatorChallenges/C1EntropyCounterexample.lean:48 (same declaration text).

12. def OAI.Problem340.totalRealHomologySpectralRadius line 55

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