OAI/Combinatorics/Progressions/Dynamics/AllocatedExternalCandidatePrecenterPaths.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.score_of_heq line 34
  2. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.precenterChart line 50
  3. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.precenterCandidate line 55
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.precenterChart_mem line 60
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.precenterCandidate_mem line 65
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.precenterChart_path line 72
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.precenterChart_center line 77
  8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.precenterChart_keep line 81
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.precenterChart_frozen line 86
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.precenterCandidate_score line 90
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.precenterCandidate_score_mem_eq line 94