OAI/NumberTheory/Jacobsthal/Partitions/CompactSelectedPartition.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.retained_no_high line 16
2. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.allowed_of_uncapped_prefix_ceiling line 23
3. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.allowed_iff_uncapped_no_high line 42
4. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.retained_eq_nonhigh line 53
5. theorem OAI.Erdos970.NumberTheoryLean.PrimeFamilyOccupation.uncapped_sum_partition line 61
6. theorem OAI.Erdos970.NumberTheoryLean.CompactSelectedPartition.selected_uncapped_partition line 84
7. theorem OAI.Erdos970.NumberTheoryLean.CompactSelectedPartition.selected_uncapped_le line 93