OAI/Combinatorics/RamseyFive/Geometry/PlanePublicDefs.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ProjectiveRestriction.planeHidden line 15
2. def OAI.SharpRamseyFive.ProjectiveRestriction.planeEnclosure line 18
3. abbrev OAI.SharpRamseyFive.ProjectiveRestriction.PlanePublicTape line 20
4. abbrev OAI.SharpRamseyFive.ProjectiveRestriction.PlanePublicMessage line 22
5. def OAI.SharpRamseyFive.ProjectiveRestriction.planePublicLaw line 25
6. def OAI.SharpRamseyFive.ProjectiveRestriction.planePublicDecoded line 28
7. def OAI.SharpRamseyFive.ProjectiveRestriction.planePublicEncoded line 31
8. def OAI.SharpRamseyFive.ProjectiveRestriction.planePublicCost line 40
9. lemma OAI.SharpRamseyFive.ProjectiveRestriction.planePublic_encoded_eq line 45
10. theorem OAI.SharpRamseyFive.ProjectiveRestriction.eventually_plane_public line 67