OAI/Combinatorics/Ryser/Geometry/Cardinality.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.card_point line 12
  2. theorem OAI.RyserCoveringCounterexample.card_direction line 16
  3. theorem OAI.RyserCoveringCounterexample.card_affineLine line 20
  4. theorem OAI.RyserCoveringCounterexample.card_projectivePoint line 24
  5. theorem OAI.RyserCoveringCounterexample.card_projectiveLine line 29
  6. def OAI.RyserCoveringCounterexample.linePointEquiv line 35
  7. theorem OAI.RyserCoveringCounterexample.card_linePoints line 66
  8. theorem OAI.RyserCoveringCounterexample.card_projection_fiber line 70
  9. def OAI.RyserCoveringCounterexample.affinePencilFiniteEquiv line 75
  10. def OAI.RyserCoveringCounterexample.affinePencilInfiniteEquiv line 86
  11. theorem OAI.RyserCoveringCounterexample.card_affinePencil_finite line 97
  12. theorem OAI.RyserCoveringCounterexample.card_affinePencil_infinite line 102
  13. theorem OAI.RyserCoveringCounterexample.projectiveLinePoints_some line 107
  14. theorem OAI.RyserCoveringCounterexample.projectiveLinePoints_none line 114
  15. theorem OAI.RyserCoveringCounterexample.projectivePencil_finite line 122
  16. theorem OAI.RyserCoveringCounterexample.projectivePencil_infinite line 130
  17. theorem OAI.RyserCoveringCounterexample.card_projectiveLinePoints line 137
  18. theorem OAI.RyserCoveringCounterexample.card_projectivePencil line 147