OAI/Combinatorics/BalancedRyser/Probability/ScheduledMarksBridge.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.ScheduledMarksBridge.rankMark line 16
  2. def OAI.Balanced.ScheduledMarksBridge.rankCount line 23
  3. theorem OAI.Balanced.ScheduledMarksBridge.marked_iff_fraction line 27
  4. def OAI.Balanced.ScheduledMarksBridge.orderedArray line 37
  5. theorem OAI.Balanced.ScheduledMarksBridge.population_prefix line 42
  6. theorem OAI.Balanced.ScheduledMarksBridge.rankMark_inl line 49
  7. theorem OAI.Balanced.ScheduledMarksBridge.rankMark_inr line 58
  8. theorem OAI.Balanced.ScheduledMarksBridge.rankCount_eq_sourceMarkCount line 70
  9. theorem OAI.Balanced.ScheduledMarksBridge.rankCount_cast line 85
  10. def OAI.Balanced.ScheduledMarksBridge.populationOrder line 93
  11. theorem OAI.Balanced.ScheduledMarksBridge.arrayMarkCount_eq_sourceMarkCount line 96