OAI/Combinatorics/ListHadwiger/HistoryBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.Footprint.History.firstPhase line 10
  2. def OAI.LinearListHadwiger.Footprint.History.secondPhase line 12
  3. lemma OAI.LinearListHadwiger.Footprint.History.phase_decomposition line 15
  4. lemma OAI.LinearListHadwiger.Footprint.History.firstPhase_degenerate line 25
  5. lemma OAI.LinearListHadwiger.Footprint.History.secondPhase_degenerate line 31
  6. lemma OAI.LinearListHadwiger.Footprint.History.secondPhase_first_neighbors line 37
  7. lemma OAI.LinearListHadwiger.Footprint.History.footprint_degenerate line 48
  8. lemma OAI.LinearListHadwiger.Footprint.History.footprint_external_neighbors line 76
  9. theorem OAI.LinearListHadwiger.Footprint.History.footprint_deletion_data line 83
  10. theorem OAI.LinearListHadwiger.SmallList.additive_deletion_or_obstruction line 112
  11. theorem OAI.LinearListHadwiger.Footprint.History.list_loss_or_obstruction line 150