OAI/Probability/BinarySweep/Mixing/BinarySplitChoices.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.BinarySplit.fillSlot line 17
  2. lemma OAI.BinaryCoordinateSweeps.BinarySplit.fillSlot_other line 20
  3. def OAI.BinaryCoordinateSweeps.BinarySplit.leftOutsideEquiv line 24
  4. def OAI.BinaryCoordinateSweeps.BinarySplit.rightOutsideEquiv line 46
  5. def OAI.BinaryCoordinateSweeps.BinarySplit.rowChoices line 68
  6. def OAI.BinaryCoordinateSweeps.BinarySplit.columnChoices line 70
  7. def OAI.BinaryCoordinateSweeps.BinarySplit.joinChoices line 73
  8. def OAI.BinaryCoordinateSweeps.BinarySplit.choicesEquiv line 78
  9. lemma OAI.BinaryCoordinateSweeps.BinarySplit.rowChoices_at line 106
  10. lemma OAI.BinaryCoordinateSweeps.BinarySplit.columnChoices_at line 115
  11. lemma OAI.BinaryCoordinateSweeps.BinarySplit.layer_left line 124
  12. lemma OAI.BinaryCoordinateSweeps.BinarySplit.layer_right line 146
  13. lemma OAI.BinaryCoordinateSweeps.BinarySplit.layer_left_congr line 169
  14. lemma OAI.BinaryCoordinateSweeps.BinarySplit.layer_right_congr line 179
  15. theorem OAI.BinaryCoordinateSweeps.BinarySplit.binarySweep_split line 189