OAI/NumberTheory/Jacobsthal/Partitions/IntervalCuts.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Erdos970.ErdosHyperbolaFourier.lowerCutline 12 - def
OAI.Erdos970.ErdosHyperbolaFourier.upperCutline 15 - theorem
OAI.Erdos970.ErdosHyperbolaFourier.lowerCut_le_iffline 17 - theorem
OAI.Erdos970.ErdosHyperbolaFourier.lt_upperCut_iffline 21 - theorem
OAI.Erdos970.ErdosHyperbolaFourier.lowerCut_boundsline 25 - theorem
OAI.Erdos970.ErdosHyperbolaFourier.upperCut_boundsline 34 - theorem
OAI.Erdos970.ErdosHyperbolaFourier.cut_count_errorline 38