OAI/Combinatorics/Progressions/Linear/MarkedLieSpan.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.markedLieSpan line 11
2. theorem OAI.Erdos3.markedLieSpan_antitone line 15
3. theorem OAI.Erdos3.markedLieSpan_lie_mem line 22
4. theorem OAI.Erdos3.markedLieSpan_leaf line 40
5. theorem OAI.Erdos3.markedLieSpan_zero_marked line 44
6. theorem OAI.Erdos3.markedLieSpan_le_layer line 51
7. theorem OAI.Erdos3.markedLieSpan_top_le_ker line 60
8. theorem OAI.Erdos3.markedLieSpan_marked_terminal line 80