OAI/Combinatorics/SecondNeighborhood/MatchingExchange.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SeymourSecondNeighborhood.Bipartite.exchange_matching_subset line 11
2. theorem OAI.SeymourSecondNeighborhood.Bipartite.exchange_matching_insert line 17
3. theorem OAI.SeymourSecondNeighborhood.Bipartite.exists_matching_saturating_left_of_card_lt line 43
4. theorem OAI.SeymourSecondNeighborhood.Bipartite.exists_matching_one_larger_saturating_left line 115