OAI/Combinatorics/BalancedRyser/Deletion/ConfigurationDeletion.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.Configuration.choice_line_injective_of_valid_compatible line 13
  2. theorem OAI.Balanced.Configuration.splitLines_filter_direction line 25
  3. theorem OAI.Balanced.Configuration.card_splitLines_filter_direction line 47
  4. theorem OAI.Balanced.Configuration.splitLines_disjoint_constituents line 57
  5. theorem OAI.Balanced.Configuration.deletedLines_filter_direction line 67
  6. theorem OAI.Balanced.Configuration.deletedLines_isDeletionSet line 86
  7. theorem OAI.Balanced.Configuration.core_eq_uncoveredBy line 103
  8. theorem OAI.Balanced.Configuration.core_eq_uncoveredPoints line 105
  9. theorem OAI.Balanced.Configuration.corePencilEvent_iff_coreConcentration line 107