OAI/Combinatorics/Progressions/Linear/ActualOrdinaryPointwiseSpanning.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.NilpotentLieFiltration.associatedGradedMap_basis_logHeight line 21
  2. theorem OAI.Erdos3.NilpotentLieFiltration.exists_associatedGradedMap_comap_bounded_spanning line 31
  3. def OAI.Erdos3.NilpotentLieFiltration.gradedImageSpanningFamily line 83
  4. theorem OAI.Erdos3.NilpotentLieFiltration.gradedImageSpanningFamily_span line 86
  5. theorem OAI.Erdos3.NilpotentLieFiltration.gradedImageSpanningFamily_logHeight line 99
  6. theorem OAI.Erdos3.NilpotentLieFiltration.gradedImage_bounded_spanning line 110
  7. theorem OAI.Erdos3.NilpotentLieFiltration.gradedImagePointwiseSpanning_heightBound line 137
  8. theorem OAI.Erdos3.NilpotentLieFiltration.pointwiseSpanningIndex_card_le line 149
  9. def OAI.Erdos3.NilpotentLieFiltration.gradedImagePointwiseSpanningFamily line 169
  10. theorem OAI.Erdos3.NilpotentLieFiltration.gradedImagePointwiseSpanningFamily_span line 176
  11. theorem OAI.Erdos3.NilpotentLieFiltration.gradedImagePointwiseSpanningFamily_height line 190
  12. theorem OAI.Erdos3.NilpotentLieFiltration.gradedImagePointwiseSpanningFamily_controlled line 204
  13. def OAI.Erdos3.NilpotentLieFiltration.ordinaryImagePointwiseBudget line 244
  14. theorem OAI.Erdos3.NilpotentLieFiltration.sectionInput_nonneg line 247
  15. theorem OAI.Erdos3.NilpotentLieFiltration.ordinaryImagePointwiseBudget_source line 252
  16. theorem OAI.Erdos3.NilpotentLieFiltration.ordinaryImagePointwiseBudget_target line 259
  17. theorem OAI.Erdos3.NilpotentLieFiltration.ordinaryImagePointwiseBudget_height line 266
  18. theorem OAI.Erdos3.NilpotentLieFiltration.ordinaryImagePointwiseBudget_ge line 273
  19. theorem OAI.Erdos3.NilpotentLieFiltration.symbolCount_le_sectionInput line 277
  20. theorem OAI.Erdos3.NilpotentLieFiltration.ordinaryGradedImagePointwiseSpanning_controlled line 292