OAI/Combinatorics/BalancedRyser/Deletion/SelectedDeletionCoordinates.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.SelectedDeletionCoordinates.SingleOffsets line 16
  2. abbrev OAI.Balanced.SelectedDeletionCoordinates.SplitOffsets line 17
  3. def OAI.Balanced.SelectedDeletionCoordinates.offsetPairEquiv line 19
  4. def OAI.Balanced.SelectedDeletionCoordinates.roles line 25
  5. theorem OAI.Balanced.SelectedDeletionCoordinates.roles_injective line 29
  6. theorem OAI.Balanced.SelectedDeletionCoordinates.mem_selected_deletedLines line 40
  7. theorem OAI.Balanced.SelectedDeletionCoordinates.selected_deletedLines_eq_assemble line 61
  8. theorem OAI.Balanced.SelectedDeletionCoordinates.selected_deletedLines_eq_iff line 77
  9. theorem OAI.Balanced.SelectedDeletionCoordinates.jointMass_eq_uniform_average line 92
  10. theorem OAI.Balanced.SelectedDeletionCoordinates.card_mergedPairs line 109
  11. theorem OAI.Balanced.SelectedDeletionCoordinates.sum_fiberMass line 114
  12. theorem OAI.Balanced.SelectedDeletionCoordinates.deletionJointMass_eq_fiber_sum line 128