OAI/Combinatorics/RamseyFive/Geometry/CoreGeometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.CoreGeometry.rep_mem_iff line 14
2. theorem OAI.SharpRamseyFive.CoreGeometry.subspace_mass_cap line 18
3. lemma OAI.SharpRamseyFive.CoreGeometry.geometric_card_bound line 49
4. theorem OAI.SharpRamseyFive.CoreGeometry.core_dimension_mass line 62
5. lemma OAI.SharpRamseyFive.CoreGeometry.rank_from_light_mass line 76
6. theorem OAI.SharpRamseyFive.CoreGeometry.core_dimension_lower line 110
7. def OAI.SharpRamseyFive.CoreGeometry.InRectangle line 132
8. lemma OAI.SharpRamseyFive.CoreGeometry.orthogonal_rank_sum line 135
9. theorem OAI.SharpRamseyFive.CoreGeometry.open_band_impossible line 141
10. lemma OAI.SharpRamseyFive.CoreGeometry.integer_band_complement line 148
11. theorem OAI.SharpRamseyFive.CoreGeometry.integer_band_rectangle line 157
12. theorem OAI.SharpRamseyFive.CoreGeometry.high_band_rectangles line 170
13. def OAI.SharpRamseyFive.CoreGeometry.RectangleCharge line 223
14. theorem OAI.SharpRamseyFive.CoreGeometry.rectangle_charge_count line 228
15. theorem OAI.SharpRamseyFive.CoreGeometry.expected_rectangle_charge line 255