OAI/Combinatorics/UniformKServer/LaminarTransport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniformKServer.LaminarTransport.bit line 18
  2. def OAI.UniformKServer.LaminarTransport.cross line 19
  3. def OAI.UniformKServer.LaminarTransport.mass line 20
  4. def OAI.UniformKServer.LaminarTransport.crossings line 21
  5. def OAI.UniformKServer.LaminarTransport.objective line 23
  6. def OAI.UniformKServer.LaminarTransport.Laminar line 26
  7. theorem OAI.UniformKServer.LaminarTransport.cross_swap_le line 29
  8. theorem OAI.UniformKServer.LaminarTransport.sum_swap line 47
  9. theorem OAI.UniformKServer.LaminarTransport.crossings_swap line 65
  10. theorem OAI.UniformKServer.LaminarTransport.no_opposite line 72
  11. theorem OAI.UniformKServer.LaminarTransport.cut_identity line 92
  12. theorem OAI.UniformKServer.LaminarTransport.matching_exists line 122