OAI/Combinatorics/Progressions/Estimates/FullTaggedRationalRetraction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rationalMatrix_real_range_eq_coordinateSpan line 11
  2. theorem OAI.Erdos3.rationalMatrix_real_fixes_coordinateSpan line 18
  3. theorem OAI.Erdos3.rationalMatrix_real_retraction line 41
  4. theorem OAI.Erdos3.exists_bounded_rational_tag_retraction line 63
  5. theorem OAI.Erdos3.exists_bounded_real_rational_tag_retraction line 132
  6. theorem OAI.Erdos3.exists_bounded_real_rational_tag_retraction_grid line 147
  7. def OAI.Erdos3.VectorPolynomial.fullTaggedRationalLinearChart line 182
  8. def OAI.Erdos3.VectorPolynomial.fullTaggedRealMatrixProjection line 188
  9. theorem OAI.Erdos3.VectorPolynomial.fullTaggedRationalLinearChart_map line 193
  10. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineMatrixChart_top_eq_map line 206
  11. theorem OAI.Erdos3.VectorPolynomial.fullTaggedRationalLinearChart_homogeneous line 214
  12. theorem OAI.Erdos3.VectorPolynomial.fullTaggedRationalLinearChart_support line 226
  13. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.exists_bounded_rational_retractions line 234