OAI/Combinatorics/MatchingCount/Tapes/TreeSparseNeighbors.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.MatchingFPRAS.TreeTyped.SparseProgram.TableInputline 14 - def
OAI.MatchingFPRAS.TreeTyped.SparseProgram.colorTableline 16 - def
OAI.MatchingFPRAS.TreeTyped.SparseProgram.colorTableRealizerline 18 - lemma
OAI.MatchingFPRAS.TreeTyped.SparseProgram.polynomial_colorTableline 32 - def
OAI.MatchingFPRAS.TreeTyped.SparseProgram.degreeline 46 - def
OAI.MatchingFPRAS.TreeTyped.SparseProgram.degreeRealizerline 47 - lemma
OAI.MatchingFPRAS.TreeTyped.SparseProgram.polynomial_degreeline 53 - def
OAI.MatchingFPRAS.TreeTyped.SparseProgram.switchTableline 60 - def
OAI.MatchingFPRAS.TreeTyped.SparseProgram.switchTableRealizerline 62 - lemma
OAI.MatchingFPRAS.TreeTyped.SparseProgram.polynomial_switchTableline 78 - lemma
OAI.MatchingFPRAS.TreeTyped.SparseProgram.colorTable_eqline 100 - lemma
OAI.MatchingFPRAS.TreeTyped.SparseProgram.switchTable_eqline 114