OAI/Combinatorics/RamseyFive/Decoding/FreshPublicValidation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.ReverseCap.fresh_public_validation line 16
2. theorem OAI.SharpRamseyFive.ReverseCap.fresh_public_domination line 30
3. def OAI.SharpRamseyFive.ReverseCap.CaptureBound line 47
4. lemma OAI.SharpRamseyFive.ReverseCap.CaptureBound.nonempty line 51
5. def OAI.SharpRamseyFive.ProjectiveIncidence.generalNextCapLaw line 66
6. theorem OAI.SharpRamseyFive.ProjectiveIncidence.reverse_after_general_capture line 77
7. theorem OAI.SharpRamseyFive.ProjectiveIncidence.general_reverse_payload line 107