OAI/Combinatorics/BalancedRyser/Incidence/AffinePencilForcing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Balanced.mem_linePoints_iff line 16
2. lemma OAI.Balanced.distinct_line_intersection_card_le_one line 19
3. lemma OAI.Balanced.pencil_line_trace_subset_point line 29
4. theorem OAI.Balanced.missing_pencil_line_occupancy_bound line 38
5. theorem OAI.Balanced.Configuration.ordinary_pencil_line_is_represented line 71