OAI/Combinatorics/RamseyFive/Geometry/AmbientPairPublic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.FiniteEntropy.public_joint_composition line 11
2. def OAI.SharpRamseyFive.ProjectiveIncidence.publicAmbientSecond line 39
3. lemma OAI.SharpRamseyFive.ProjectiveIncidence.publicAmbientSecond_law line 51
4. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.AmbientPairTape line 70
5. def OAI.SharpRamseyFive.ProjectiveIncidence.ambientPairTapeLaw line 73
6. abbrev OAI.SharpRamseyFive.ProjectiveIncidence.AmbientPairMessage line 75
7. def OAI.SharpRamseyFive.ProjectiveIncidence.ambientPairDecoded line 79
8. def OAI.SharpRamseyFive.ProjectiveIncidence.ambientPairEncoded line 84
9. def OAI.SharpRamseyFive.ProjectiveIncidence.ambientPairCost line 94
10. lemma OAI.SharpRamseyFive.ProjectiveIncidence.ambientPair_exact line 100
11. theorem OAI.SharpRamseyFive.ProjectiveIncidence.ambientPair_law line 114
12. lemma OAI.SharpRamseyFive.ProjectiveIncidence.ambientPair_prefixes line 134