OAI/Combinatorics/SquareDifference/OrderedBlock.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SquareDifference.orderedLowError line 15
2. lemma OAI.SquareDifference.orderedLowError_nonneg line 18
3. lemma OAI.SquareDifference.ordered_low_cost line 24
4. lemma OAI.SquareDifference.ordered_interval_full line 47
5. lemma OAI.SquareDifference.blockLift_expect line 76