OAI/Combinatorics/RamseyFive/Geometry/Cores.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.CoreGeometry.firstCore line 14
2. def OAI.SharpRamseyFive.CoreGeometry.secondCore line 17
3. lemma OAI.SharpRamseyFive.CoreGeometry.conditional_flag_annihilation line 20
4. lemma OAI.SharpRamseyFive.CoreGeometry.firstCore_self line 35
5. lemma OAI.SharpRamseyFive.CoreGeometry.secondCore_self line 43
6. theorem OAI.SharpRamseyFive.CoreGeometry.actual_integer_rectangle line 63
7. theorem OAI.SharpRamseyFive.CoreGeometry.actual_high_rectangles line 79
8. theorem OAI.SharpRamseyFive.CoreGeometry.actual_open_impossible line 97