OAI/Combinatorics/EditApproximation/Binary/BinaryCellCenters.lean
3 declarations, 0 contain sorry, 0 declared as axioms
Literal eligibility scans for the whole-cell representative list.
- theorem
OAI.EditApproximation.BinaryFraction.centerEligibilityWithWork_valueline 14 - def
OAI.EditApproximation.BinaryFraction.cellCentersWithWorkline 21 - theorem
OAI.EditApproximation.BinaryFraction.cellCentersWithWork_valueline 30