OAI/NumberTheory/Jacobsthal/Paths/SourceWitnessSeries.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.tagSourceReturn line 15
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.tagSourceReturn_measurable line 18
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceWitnessTerm line 21
4. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceWitnessTerm_isFiniteKernel line 24
5. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessRemaining line 28
6. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessRemaining_isSFiniteKernel line 31
7. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation_measure line 35
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation_at_return line 43
9. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation_outside_return line 50
10. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.firstPairs_partition line 78
11. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation_comp_captured line 84
12. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.witnessContinuation_comp_killed line 100
13. theorem OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceCycleWitness_series line 116
14. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sourceWitnessTerm_duration line 124