OAI/Combinatorics/Progressions/Linear/SplitPreimageSpanning.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.comap_eq_section_image_sup_kernel line 13
2. theorem OAI.Erdos3.span_range_sumElim line 30
3. theorem OAI.Erdos3.split_preimage_spanning line 45