OAI/Combinatorics/Progressions/Linear/WeightedFlagBasis.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.span_image_inl_of_basis_extension line 18
2. theorem OAI.Erdos3.span_range_inl_complement_basis line 39
3. theorem OAI.Erdos3.exists_basis_with_nested_supports line 64
4. def OAI.Erdos3.nestedSupportWeight line 124
5. theorem OAI.Erdos3.nestedSupportWeight_le line 127
6. theorem OAI.Erdos3.mem_nestedSupport_iff line 133
7. theorem OAI.Erdos3.exists_sorted_weighted_flag_basis line 156