OAI/NumberTheory/Jacobsthal/Paths/ActualFirstTagExistence.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.PaperOwnerHeight.sourceW_square_two_L line 13
2. theorem OAI.Erdos970.NumberTheoryLean.PaperOwnerHeight.literal_source_floor_height line 27
3. theorem OAI.Erdos970.NumberTheoryLean.PaperBinOwners.paper_bin_span line 50
4. theorem OAI.Erdos970.NumberTheoryLean.PaperBinOwners.paper_owner_unique line 70
5. theorem OAI.Erdos970.NumberTheoryLean.PaperBinOwners.paper_owner_identifies line 92
6. theorem OAI.Erdos970.NumberTheoryLean.PaperCorrectTag.paper_correct_candidate line 116
7. theorem OAI.Erdos970.NumberTheoryLean.PaperCorrectTag.paper_first_tag_correct line 140
8. theorem OAI.Erdos970.NumberTheoryLean.SourceOwnerAudit.literal_floor_owner_unique line 169
9. theorem OAI.Erdos970.ErdosTagEvent.firstTagFrom_none_iff line 188
10. theorem OAI.Erdos970.ErdosTagEvent.firstTag_exists_of_candidate line 197
11. theorem OAI.Erdos970.ErdosTagEvent.sourceTag_exists_of_candidate line 207