OAI/NumberTheory/Jacobsthal/Paths/CanonicalWordPrefix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.sigmaInputKernel line 13
2. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.sigmaInputKernel_isFinite_of_bound line 18
3. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonicalWordFirstPrefix line 23
4. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonicalWordFirstPrefix_bound line 29
5. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonicalWordFirstPrefix_isFiniteKernel line 56
6. instance OAI.Erdos970.Erdos970Dependency.MarkedVisits.canonicalWordContinuation_isFiniteKernel line 59
7. def OAI.Erdos970.Erdos970Dependency.MarkedVisits.wordFirstPrefix line 64
8. lemma OAI.Erdos970.Erdos970Dependency.MarkedVisits.wordFirstPrefix_measurable line 67