OAI/Combinatorics/Progressions/Estimates/RationalTagConstraintSpaces.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.Erdos3.VectorPolynomial.RationalTagConstraint line 12
  2. def OAI.Erdos3.VectorPolynomial.RationalTagConstraint.member line 21
  3. def OAI.Erdos3.VectorPolynomial.RationalTagConstraint.BudgetLE line 26
  4. theorem OAI.Erdos3.VectorPolynomial.RationalTagConstraint.BudgetLE.mono line 29
  5. def OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate line 35
  6. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.empty line 46
  7. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.monoB line 52
  8. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.monoBlocks line 57
  9. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.subset line 62
  10. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.singleton line 66
  11. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.trans line 73
  12. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.inter line 90
  13. theorem OAI.Erdos3.VectorPolynomial.RationalTagConstraint.retained_le_span line 119
  14. theorem OAI.Erdos3.VectorPolynomial.exists_finite_rational_tag_constraints line 152
  15. theorem OAI.Erdos3.VectorPolynomial.exists_finite_rational_tag_constraint_lists line 210
  16. theorem OAI.Erdos3.VectorPolynomial.exists_finite_rational_tagged_certificate_sets line 234
  17. theorem OAI.Erdos3.VectorPolynomial.exists_finite_rational_stage_branches line 268
  18. def OAI.Erdos3.VectorPolynomial.RationalTagConstraint.rationalSpace line 317
  19. theorem OAI.Erdos3.VectorPolynomial.RationalTagConstraint.rationalSpace_self line 321
  20. theorem OAI.Erdos3.VectorPolynomial.RationalTagConstraint.rationalSpace_of_ne line 325
  21. theorem OAI.Erdos3.VectorPolynomial.RationalTagConstraint.exists_function_spanning_logHeight line 329
  22. theorem OAI.Erdos3.VectorPolynomial.RationalTagConstraint.exists_rationalSpace_spanning line 347