OAI/Combinatorics/IndependentSets/Encoding/GapFormula.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.LargeIndependentSets.SemanticReduction.gapFormulaline 16 - instance
OAI.LargeIndependentSets.SemanticReduction.eventsNonemptyline 19 - def
OAI.LargeIndependentSets.SemanticReduction.reduceline 23 - lemma
OAI.LargeIndependentSets.SemanticReduction.completeline 27 - lemma
OAI.LargeIndependentSets.SemanticReduction.vertex_boundline 34 - theorem
OAI.LargeIndependentSets.semantic_reductionline 43