OAI/Combinatorics/BalancedRyser/Candidates/DeletedConstituentForcing.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Balanced.Configuration.on_line_iff_mem line 14
2. lemma OAI.Balanced.Configuration.constituent_ne_of_direction_ne line 18
3. theorem OAI.Balanced.Configuration.other_block_constituent_trace_le_two line 23
4. theorem OAI.Balanced.Configuration.selected_merged_pencil_card_le line 65
5. theorem OAI.Balanced.Configuration.missing_deleted_constituent_occupancy_bound line 79
6. theorem OAI.Balanced.Configuration.deleted_constituent_merged_label_selected line 157