OAI/Combinatorics/BalancedRyser/Incidence/Projective2.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.dualPoint_dualLine line 11
  2. theorem OAI.Balanced.dualLine_dualPoint line 17
  3. def OAI.Balanced.projectiveDuality line 23
  4. theorem OAI.Balanced.affineDualPoint_injective line 29
  5. theorem OAI.Balanced.projective_incident_dual line 34
  6. theorem OAI.Balanced.missedProjective_eq_disjSum line 65
  7. theorem OAI.Balanced.card_missedProjective line 81
  8. theorem OAI.Balanced.card_dualPointSet line 88
  9. theorem OAI.Balanced.mem_skew_dualLine_iff line 92
  10. theorem OAI.Balanced.card_skew_dualPointSet line 102
  11. theorem OAI.Balanced.card_skew_dualPointSet_exact line 109
  12. theorem OAI.Balanced.card_skew_dualPointSet_le line 114
  13. theorem OAI.Balanced.card_dualPointSet_on_line line 121
  14. theorem OAI.Balanced.dual_line_bound_gives_pencil line 135