OAI/Combinatorics/Progressions/Geometry/AllocatedExternalLocalChartKeepBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.withKeep line 33
  2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.withKeep_self line 49
  3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.withKeep_slice_transport line 51
  4. def OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.withKeep line 82
  5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.withKeep_score line 87
  6. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.withKeep line 102
  7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.withKeep_chart_keep line 118
  8. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_withKeep line 121
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.slice_transport_of_eq_withKeep line 188
  10. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_chartwise_withKeep line 223
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_chartwise_withKeep_retained line 264
  12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_chartwise_withKeep_ambient line 275
  13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.withKeep_chart_fixed line 324
  14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.withKeep_polynomialSlowBound line 339
  15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.withKeep_dense line 358
  16. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.withKeep_original_dense line 366