OAI/Combinatorics/BalancedRyser/Candidates/CandidateValidityWitness.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.CandidateValidityWitness.SuccessfulOn line 11
  2. def OAI.Balanced.CandidateValidityWitness.PairWitness line 15
  3. theorem OAI.Balanced.CandidateValidityWitness.adjacent_iff_witness line 20
  4. theorem OAI.Balanced.CandidateValidityWitness.target_constituent_intersection_unique line 36
  5. theorem OAI.Balanced.CandidateValidityWitness.previous_next line 45
  6. theorem OAI.Balanced.CandidateValidityWitness.adjacent_generators_ne line 49
  7. theorem OAI.Balanced.CandidateValidityWitness.purposeful_endpoints line 58
  8. theorem OAI.Balanced.CandidateValidityWitness.used_constituents_distinct line 73
  9. theorem OAI.Balanced.CandidateValidityWitness.on_used_constituent_endpoint line 88
  10. theorem OAI.Balanced.CandidateValidityWitness.external_not_on_used_constituent line 105
  11. theorem OAI.Balanced.CandidateValidityWitness.opposite_witness_not_generator line 117
  12. theorem OAI.Balanced.CandidateValidityWitness.external_witness_not_generator line 132
  13. theorem OAI.Balanced.CandidateValidityWitness.pairWitness_partner_unique line 143
  14. theorem OAI.Balanced.CandidateValidityWitness.external_witness_directions_distinct line 158
  15. def OAI.Balanced.CandidateValidityWitness.OppositeWitness line 172
  16. def OAI.Balanced.CandidateValidityWitness.ExternalDoubleWitness line 176
  17. theorem OAI.Balanced.CandidateValidityWitness.not_valid_has_bounded_witness line 183
  18. theorem OAI.Balanced.CandidateValidityWitness.bounded_witness_not_valid line 217
  19. theorem OAI.Balanced.CandidateValidityWitness.not_valid_iff_bounded_witness line 242
  20. theorem OAI.Balanced.CandidateValidityWitness.constituent_target_iff line 250