OAI/Combinatorics/BalancedRyser/Incidence/CorePencilFieldTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.FieldTransport.projectivePointEquiv line 12
2. theorem OAI.Balanced.FieldTransport.throughProjective_transport line 15
3. theorem OAI.Balanced.FieldTransport.pencilSize_transport line 29
4. theorem OAI.Balanced.FieldTransport.uncoveredPoints_transport line 37
5. theorem OAI.Balanced.FieldTransport.corePencilEvent_map line 42
6. theorem OAI.Balanced.FieldTransport.corePencilEvent_transport line 59
7. theorem OAI.Balanced.FieldTransport.core_pencil_failure_probability_transport line 67
8. theorem OAI.Balanced.FieldTransport.same_order_core_pencil_transport line 74