OAI/NumberTheory/Jacobsthal/Paths/PairCaptureProjection.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawLast line 16
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawLast_measurable line 18
3. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_last_pair line 20
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawExtension_restricted_last_pair line 36
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairCaptured line 42
6. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairKilled line 45
7. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairCaptured_isFiniteKernel line 48
8. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.fullPairKilled_isFiniteKernel line 53
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.embedOdd_regeneration_preimage line 58
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costCaptured_fullPair_projection line 60
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.costKilled_fullPair_projection line 66
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawCapturedPair_projection line 72
13. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.rawKilledPair_projection line 77
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory_zero line 82
15. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstReturnHistory_zero_projection line 90