OAI/Combinatorics/SecondNeighborhood/ExtremalCounting.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SeymourSecondNeighborhood.Extremal.uncoveredCountline 15 - def
OAI.SeymourSecondNeighborhood.Extremal.objectiveline 18 - theorem
OAI.SeymourSecondNeighborhood.Extremal.uncoveredCount_add_imagesline 21 - theorem
OAI.SeymourSecondNeighborhood.Extremal.uncoveredZ_card_leline 31 - theorem
OAI.SeymourSecondNeighborhood.Extremal.objective_lt_of_pruningline 40 - theorem
OAI.SeymourSecondNeighborhood.Extremal.exists_maximizing_pairline 53