OAI/Dynamics/EntropyCounterexample/ClockQuotient.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem340.ClockQuotient.periodize line 15
2. lemma OAI.Problem340.ClockQuotient.periodic_periodize line 18
3. lemma OAI.Problem340.ClockQuotient.locallyFinite_translated_strips line 36
4. lemma OAI.Problem340.ClockQuotient.locallyFinite_translated_supports line 47
5. lemma OAI.Problem340.ClockQuotient.continuous_periodize line 56
6. lemma OAI.Problem340.ClockQuotient.periodize_eq_tsum line 66
7. lemma OAI.Problem340.ClockQuotient.periodize_eq_on_fundamental_strip line 74
8. lemma OAI.Problem340.ClockQuotient.periodize_eq_toIcoMod line 93
9. lemma OAI.Problem340.ClockQuotient.periodize_mem_Icc line 103
10. def OAI.Problem340.ClockQuotient.liftPeriodic line 111
11. lemma OAI.Problem340.ClockQuotient.liftPeriodic_coe line 115
12. lemma OAI.Problem340.ClockQuotient.continuous_liftPeriodic line 120
13. lemma OAI.Problem340.ClockQuotient.liftPeriodic_eq_liftIco line 130
14. lemma OAI.Problem340.ClockQuotient.continuous_liftIco_of_periodic line 140
15. def OAI.Problem340.ClockQuotient.liftPeriodize line 147
16. lemma OAI.Problem340.ClockQuotient.liftPeriodize_coe line 150
17. lemma OAI.Problem340.ClockQuotient.continuous_liftPeriodize line 155
18. lemma OAI.Problem340.ClockQuotient.liftPeriodize_eq_liftIco line 163
19. lemma OAI.Problem340.ClockQuotient.continuous_liftIco_of_strip_support line 181