OAI/Combinatorics/RamseyFive/Marking/DomainTransport.lean
10 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SharpRamseyFive.Marking.swapDomainline 17 - lemma
OAI.SharpRamseyFive.Marking.mem_swapDomain_iffline 21 - lemma
OAI.SharpRamseyFive.Marking.swapDomain_first_cardline 28 - lemma
OAI.SharpRamseyFive.Marking.swapDomain_second_cardline 37 - lemma
OAI.SharpRamseyFive.Marking.swapDomain_first_partnersline 46 - lemma
OAI.SharpRamseyFive.Marking.swapDomain_second_partnersline 56 - lemma
OAI.SharpRamseyFive.Marking.ReverseCaps.swapline 67 - structure
OAI.SharpRamseyFive.Marking.HighCapsline 71 - lemma
OAI.SharpRamseyFive.Marking.HighCaps.swapline 78 - lemma
OAI.SharpRamseyFive.Marking.marking_highCapsline 90