OAI/Combinatorics/SharpRamsey/Construction/InitialRectangles.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.InitialRectangles.IsRectangle line 32
2. lemma OAI.SharpLogRamsey.InitialRectangles.card_points line 36
3. lemma OAI.SharpLogRamsey.InitialRectangles.card_rectangle_le line 42
4. lemma OAI.SharpLogRamsey.InitialRectangles.card_subspaces_le line 63
5. lemma OAI.SharpLogRamsey.InitialRectangles.sum_powers_le_two line 78
6. lemma OAI.SharpLogRamsey.InitialRectangles.card_rectangle_bound line 92
7. lemma OAI.SharpLogRamsey.InitialRectangles.card_flags_lower line 117
8. lemma OAI.SharpLogRamsey.InitialRectangles.finite_flags line 128
9. lemma OAI.SharpLogRamsey.InitialRectangles.finite_subspaces line 130