OAI/Combinatorics/BalancedRyser/Deletion/UniformDeletionEnumeration.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.UniformDeletionEnumeration.lineEmbedding line 15
  2. def OAI.Balanced.UniformDeletionEnumeration.selectedLines line 25
  3. theorem OAI.Balanced.UniformDeletionEnumeration.mem_selectedLines line 29
  4. theorem OAI.Balanced.UniformDeletionEnumeration.selectedLines_filter line 44
  5. theorem OAI.Balanced.UniformDeletionEnumeration.selectedLines_isDeletionSet line 65
  6. def OAI.Balanced.UniformDeletionEnumeration.deletionOutcome line 71
  7. theorem OAI.Balanced.UniformDeletionEnumeration.deletionOutcome_surjective line 74
  8. def OAI.Balanced.UniformDeletionEnumeration.lineRelabel line 109
  9. def OAI.Balanced.UniformDeletionEnumeration.arrayRelabel line 115
  10. theorem OAI.Balanced.UniformDeletionEnumeration.selectedLines_relabel line 121
  11. theorem OAI.Balanced.UniformDeletionEnumeration.exists_relabel_outcomes line 128
  12. theorem OAI.Balanced.UniformDeletionEnumeration.outcome_fiber_card_eq line 145
  13. theorem OAI.Balanced.UniformDeletionEnumeration.expect_deletionOutcome line 166
  14. theorem OAI.Balanced.UniformDeletionEnumeration.deletionOutcome_probability line 178
  15. def OAI.Balanced.UniformDeletionEnumeration.tokenEquiv line 185
  16. def OAI.Balanced.UniformDeletionEnumeration.orderingEquiv line 195
  17. theorem OAI.Balanced.UniformDeletionEnumeration.expect_ordering line 209
  18. theorem OAI.Balanced.UniformDeletionEnumeration.expect_uniform_deletion_and_order line 217
  19. def OAI.Balanced.UniformDeletionEnumeration.canonicalOffsets line 233
  20. theorem OAI.Balanced.UniformDeletionEnumeration.expect_uniform_deletion_and_order_of_le line 236
  21. theorem OAI.Balanced.UniformDeletionEnumeration.expect_originalExperiment line 244
  22. theorem OAI.Balanced.UniformDeletionEnumeration.orderedLine_eq_nextLine line 253
  23. theorem OAI.Balanced.UniformDeletionEnumeration.card_tokens line 261
  24. def OAI.Balanced.UniformDeletionEnumeration.timeToToken line 264
  25. def OAI.Balanced.UniformDeletionEnumeration.timeOrderingEquiv line 267
  26. theorem OAI.Balanced.UniformDeletionEnumeration.expect_originalExperiment_time line 280