OAI/Combinatorics/BalancedRyser/Selection/SelectionAuxiliaryTracks.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Selection.Process.censoredDomainNumerator line 15
  2. def OAI.Balanced.Selection.Process.censoredDegreeNumerator line 22
  3. def OAI.Balanced.Selection.Process.domainTrackIncrement line 29
  4. def OAI.Balanced.Selection.Process.degreeTrackIncrement line 39
  5. def OAI.Balanced.Selection.Process.domainTrack line 49
  6. def OAI.Balanced.Selection.Process.degreeTrack line 54
  7. theorem OAI.Balanced.Selection.Process.domainTrack_zero line 59
  8. theorem OAI.Balanced.Selection.Process.degreeTrack_zero line 64
  9. theorem OAI.Balanced.Selection.Process.domainTrack_succ_sub line 69
  10. theorem OAI.Balanced.Selection.Process.degreeTrack_succ_sub line 75
  11. theorem OAI.Balanced.Selection.Process.positive_snapshot_surviving_step line 83
  12. theorem OAI.Balanced.Selection.Process.ae_snapshot_positive_steps line 111
  13. theorem OAI.Balanced.Selection.Process.domainTrack_agreement_of_positive_steps line 126
  14. theorem OAI.Balanced.Selection.Process.degreeTrack_agreement_of_positive_steps line 157
  15. theorem OAI.Balanced.Selection.Process.ae_domainTrack_agreement line 192
  16. theorem OAI.Balanced.Selection.Process.ae_degreeTrack_agreement line 200