OAI/Combinatorics/BalancedRyser/Incidence/StabilitySkewCountLemmas.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.skewThroughExcept line 14
  2. theorem OAI.Balanced.mem_skewThroughExcept line 18
  3. theorem OAI.Balanced.card_nonSkew_pencil_erase_le line 24
  4. theorem OAI.Balanced.card_skewThroughExcept_ge line 47
  5. theorem OAI.Balanced.skewThroughExcept_disjoint line 64
  6. theorem OAI.Balanced.missing_mul_order_sub_offLine_le_skew line 74
  7. theorem OAI.Balanced.card_projectiveLines line 117
  8. theorem OAI.Balanced.skewProjective_eq_compl_pencils line 122
  9. theorem OAI.Balanced.projective_order_le_skew_add_pencils line 127
  10. theorem OAI.Balanced.card_skewProjective_pos_of_card_le_order line 139
  11. theorem OAI.Balanced.exists_skewProjective_of_card_le_order line 145
  12. theorem OAI.Balanced.card_skew_dualPointSet_pos line 151