OAI/Combinatorics/EditApproximation/Binary/BinaryPreparedLocalGroups.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Whole-cell query groups with fully constructed endpoint grids.

  1. theorem OAI.EditApproximation.BinaryFraction.prepared_cellDraw_roundtrip line 11
  2. def OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleWithWork line 18
  3. theorem OAI.EditApproximation.BinaryFraction.preparedLocalGroupScaleWithWork_value line 36
  4. def OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsWithWork line 61
  5. theorem OAI.EditApproximation.BinaryFraction.flatMap_filter_condition line 79

    Also declared: OAI/Combinatorics/EditApproximation/Binary/BinaryLocalGroupActions.lean:90 (same declaration text).

  6. theorem OAI.EditApproximation.BinaryFraction.preparedLocalCellGroupsWithWork_value line 89