OAI/Combinatorics/BalancedRyser/Deletion/GeometricDeletionCounting.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.GeometricDeletionCounting.offsetsAt line 15
  2. theorem OAI.Balanced.GeometricDeletionCounting.mem_offsetsAt line 18
  3. def OAI.Balanced.GeometricDeletionCounting.assemble line 22
  4. theorem OAI.Balanced.GeometricDeletionCounting.mem_assemble line 25
  5. theorem OAI.Balanced.GeometricDeletionCounting.offsetsAt_assemble line 29
  6. theorem OAI.Balanced.GeometricDeletionCounting.assemble_offsetsAt line 34
  7. theorem OAI.Balanced.GeometricDeletionCounting.card_offsetsAt line 40
  8. def OAI.Balanced.GeometricDeletionCounting.deletionEquivFamilies line 56
  9. theorem OAI.Balanced.GeometricDeletionCounting.card_deletionSet line 71
  10. theorem OAI.Balanced.GeometricDeletionCounting.nonempty_deletionSet line 77
  11. theorem OAI.Balanced.GeometricDeletionCounting.nonempty_deletionSet_iff line 83
  12. theorem OAI.Balanced.GeometricDeletionCounting.uniformDeletionMass_eq line 94
  13. theorem OAI.Balanced.GeometricDeletionCounting.card_deleted_lines line 99