OAI/Combinatorics/BalancedRyser/Local/ReuseSourceWitness.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.ReusePrescription.sourcePoint line 11
  2. theorem OAI.Balanced.ReusePrescription.card_source_positions line 17
  3. def OAI.Balanced.ReusePrescription.SourceEvent line 32
  4. theorem OAI.Balanced.ReusePrescription.tuple_eq_of_matches line 38
  5. theorem OAI.Balanced.ReusePrescription.code_eq_of_matches_slot_eq line 44
  6. theorem OAI.Balanced.ReusePrescription.target_line_eq_of_matches line 51
  7. theorem OAI.Balanced.ReusePrescription.sourcePoint_injective_of_matches line 60
  8. theorem OAI.Balanced.ReusePrescription.target_injective_of_matches line 79
  9. theorem OAI.Balanced.ReusePrescription.sourceEvent_of_matches line 91
  10. theorem OAI.Balanced.ReusePrescription.exists_source_witness line 101
  11. theorem OAI.Balanced.ReusePrescription.selected_source_list_le line 109
  12. theorem OAI.Balanced.ReusePrescription.selected_reuse_le_source_witness_sum line 123
  13. theorem OAI.Balanced.ReusePrescription.source_witness_sum_le_relaxed line 141