OAI/Combinatorics/BalancedRyser/Incidence/SinglePencilObstruction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.Configuration.NonsplitThrough line 13
2. theorem OAI.Balanced.Configuration.constituent_mem line 19
3. theorem OAI.Balanced.Configuration.split_ne_constituent line 23
4. theorem OAI.Balanced.Configuration.nonsplit_trace line 29
5. theorem OAI.Balanced.Configuration.nonsplit_pencil_not_cover line 76
6. theorem OAI.Balanced.Configuration.one_split_cover_impossible line 91