OAI/Computability/BinPacking/Packing/GoodAnchorBound.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinPackingGap.RoleItem line 15
  2. theorem OAI.BinPackingGap.roleItem_label_count line 18
  3. structure OAI.BinPackingGap.RoleLabelData line 45
  4. theorem OAI.BinPackingGap.RoleLabelData.row_count line 57
  5. theorem OAI.BinPackingGap.RoleLabelData.anchor_count line 63
  6. theorem OAI.BinPackingGap.RoleLabelData.local_count line 69
  7. def OAI.BinPackingGap.RoleLabelData.of_valid line 75
  8. def OAI.BinPackingGap.Packing.roleItemAt line 93
  9. theorem OAI.BinPackingGap.Packing.roleItemAt_injective line 97
  10. theorem OAI.BinPackingGap.Packing.roleItemAt_labels line 102
  11. theorem OAI.BinPackingGap.Packing.roleItemAt_labels_le line 116
  12. theorem OAI.BinPackingGap.Packing.outside_roleItems_image_subset line 126
  13. theorem OAI.BinPackingGap.Packing.outside_roleItems_card_le line 143
  14. theorem OAI.BinPackingGap.Coverage.goodTuplesAt_iff_roleLabels line 155
  15. def OAI.BinPackingGap.Coverage.badRoleAnchors line 176
  16. theorem OAI.BinPackingGap.Coverage.mem_badRoleAnchors line 183
  17. theorem OAI.BinPackingGap.Coverage.badRoleAnchors_image_eq line 195
  18. theorem OAI.BinPackingGap.Coverage.badRoleAnchors_card line 225
  19. theorem OAI.BinPackingGap.Coverage.badAnchorsAt_card_le line 246
  20. theorem OAI.BinPackingGap.Coverage.badAnchorsAt_subset_card_le line 268
  21. theorem OAI.BinPackingGap.Coverage.anchor_subset_loss_le line 274
  22. theorem OAI.BinPackingGap.Coverage.badAnchors_global_card_le line 284