OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidateRefinementLabels.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.refineSlice line 37
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.refineSlice_path line 53
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.refineSlice_centerLift line 56
  4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.refineSlice_integerChart line 59
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.refineSlice_chartValues line 62
  6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.refineSlice_parameter line 65
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.refineSlice_physical line 68
  8. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.refineSlice line 90
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.refineSlice_orbit line 96
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.refineSlice_value line 99
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.refineSlice_score line 102
  12. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement line 115
  13. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.problem line 140
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.problem_productive line 157
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.problem_chart_path line 159
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.problem_chartValues line 162
  17. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.problem_physical line 167
  18. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.problem_ambientScore line 172
  19. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.conclusion line 179
  20. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_common_keep_refinement line 237
  21. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_common_keep_refinement_exp line 277
  22. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.restrictPaths line 346
  23. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.Refinement.exists_common_label line 360