OAI/Combinatorics/RamseyFive/Geometry/FlagGraph.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpRamseyFive.FlagConstruction.Space line 12
2. abbrev OAI.SharpRamseyFive.FlagConstruction.Point line 13
3. abbrev OAI.SharpRamseyFive.FlagConstruction.DualPoint line 14
4. def OAI.SharpRamseyFive.FlagConstruction.Incident line 16
5. lemma OAI.SharpRamseyFive.FlagConstruction.incident_iff line 19
6. abbrev OAI.SharpRamseyFive.FlagConstruction.Flag line 24
7. def OAI.SharpRamseyFive.FlagConstruction.graph line 27
8. lemma OAI.SharpRamseyFive.FlagConstruction.adj_iff_of_lt line 35
9. lemma OAI.SharpRamseyFive.FlagConstruction.five_independent line 40
10. theorem OAI.SharpRamseyFive.FlagConstruction.cliqueFree_five line 76
11. lemma OAI.SharpRamseyFive.FlagConstruction.independent_selector_of_not_cliqueFree line 112
12. def OAI.SharpRamseyFive.FlagConstruction.encodeRaw line 130
13. lemma OAI.SharpRamseyFive.FlagConstruction.encodeRaw_leftInverse line 133
14. theorem OAI.SharpRamseyFive.FlagConstruction.initial_consistent_stream line 140
15. lemma OAI.SharpRamseyFive.Marking.tupleIncident_comp line 159
16. lemma OAI.SharpRamseyFive.Marking.tupleConsistent_comp line 161
17. lemma OAI.SharpRamseyFive.Marking.retained_incident line 164
18. lemma OAI.SharpRamseyFive.Marking.retained_consistent line 167