OAI/Combinatorics/Progressions/Estimates/PhysicalBoundaryLabels.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Erdos3.integer_cut_side_stableline 11 - theorem
OAI.Erdos3.integer_interval_membership_stableline 24 - def
OAI.Erdos3.physicalBoxClassifyline 34 - def
OAI.Erdos3.physicalBoundaryNearline 38 - theorem
OAI.Erdos3.physicalBoxClassify_eq_some_iffline 43 - theorem
OAI.Erdos3.physicalBoxClassify_stableline 66