OAI/Combinatorics/RamseyFive/Trees/TreeOmissionLaw.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpRamseyFive.TreeCodec.expectedOmissionline 15 - lemma
OAI.SharpRamseyFive.TreeCodec.expectedOmission_nonnegline 19 - lemma
OAI.SharpRamseyFive.TreeCodec.expectedOmission_nodeline 27