OAI/Combinatorics/Progressions/Polynomial/WeightedLieDegreeLengthSpan.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.weightedLieDegreeLengthSpan line 12
2. theorem OAI.Erdos3.weightedLieDegreeLengthSpan_antitone line 15
3. theorem OAI.Erdos3.weightedLieDegreeLengthSpan_lie_mem line 22
4. theorem OAI.Erdos3.weightedLieUpperSpan_map_le_degreeLengthSpan line 39
5. theorem OAI.Erdos3.FilteredLieTree.map_eval_mem_degreeLengthSpan line 50
6. theorem OAI.Erdos3.weightedLieDegreeLengthSpan_top_le_ker line 61