OAI/Probability/BinarySweep/GridBounds/GridSplitSweep.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinaryCoordinateSweeps.GridSplit.rowPerm line 12
2. def OAI.BinaryCoordinateSweeps.GridSplit.rowPermHom line 18
3. def OAI.BinaryCoordinateSweeps.GridSplit.columnPerm line 23
4. def OAI.BinaryCoordinateSweeps.GridSplit.columnPermHom line 29
5. lemma OAI.BinaryCoordinateSweeps.GridSplit.gridLayer_left line 36
6. lemma OAI.BinaryCoordinateSweeps.GridSplit.gridLayer_right line 57
7. lemma OAI.BinaryCoordinateSweeps.GridSplit.layer_left_congr line 78
8. lemma OAI.BinaryCoordinateSweeps.GridSplit.layer_right_congr line 91
9. lemma OAI.BinaryCoordinateSweeps.GridSplit.prod_rows line 104
10. lemma OAI.BinaryCoordinateSweeps.GridSplit.prod_columns line 113
11. theorem OAI.BinaryCoordinateSweeps.GridSplit.gridSweep_split line 123