OAI/NumberTheory/Jacobsthal/Estimates/SortedRealGaps.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosMarkedStrips.gapLeft line 12
2. def OAI.Erdos970.ErdosMarkedStrips.gapRight line 15
3. theorem OAI.Erdos970.ErdosMarkedStrips.gapLeft_mem line 18
4. theorem OAI.Erdos970.ErdosMarkedStrips.gapRight_mem line 21
5. theorem OAI.Erdos970.ErdosMarkedStrips.gap_lt line 24
6. theorem OAI.Erdos970.ErdosMarkedStrips.no_mark_in_gap line 29
7. theorem OAI.Erdos970.ErdosMarkedStrips.exists_gap_of_not_mem line 41
8. theorem OAI.Erdos970.ErdosMarkedStrips.number_of_gaps_le line 74