OAI/NumberTheory/Jacobsthal/Paths/RawStableHistory.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnHistoryProperty line 16
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnHistoryProperty_measurable line 20
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturn_historyProperty line 26
4. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.selectedHistoryProperty line 35
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.selectedHistoryProperty_measurable line 39
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastRawCycle_historyProperty line 45
7. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.continuationHistoryProperty line 65
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.continuationHistoryProperty_measurable line 69
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawContinuation_historyProperty line 73
10. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedHistoryProperty line 85
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedHistoryProperty_measurable line 89
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.packedInitial_historyProperty line 95
13. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.hitHistoryProperty line 109
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.hitHistoryProperty_measurable line 113
15. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawRegFirstHit_historyProperty line 121
16. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawEvenHit_historyProperty line 136