OAI/NumberTheory/Jacobsthal/Paths/RawIncreasingPrefix.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.actualCostKernel_strict line 15
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_strict_step line 28
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_strict_coordinate line 42
4. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.increasingCosts line 61
5. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.increasingCosts_measurable line 64
6. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.increasingCosts_of_steps line 78
7. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_increasingCosts line 94
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.increasingCosts_at_start line 119
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.increasingCosts_extend line 126
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_preserves_increasing line 145
11. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnIncreasing line 151
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.returnIncreasing_measurable line 154
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawReturn_increasing line 159
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawBranchReturn_increasing line 168
15. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.selectedIncreasing line 173
16. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.selectedIncreasing_measurable line 176
17. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.lastRawCycle_increasing line 181