OAI/Probability/SKBarriers/Dynamics/BankPool.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SK.Analytic.overlap_orient_right_abs line 13
  2. theorem OAI.SK.Analytic.exists_orient_overlap line 17
  3. def OAI.SK.Analytic.orientedBankPool line 26
  4. theorem OAI.SK.Analytic.mem_orientedBankPool line 29
  5. theorem OAI.SK.Analytic.flip_mem_orientedBankPool line 34
  6. def OAI.SK.Analytic.natBankPool line 41
  7. def OAI.SK.Analytic.natBankDefault line 44
  8. theorem OAI.SK.Analytic.natBankDefault_mem line 47
  9. def OAI.SK.Analytic.blockPrior line 55
  10. theorem OAI.SK.Analytic.mem_blockPrior line 58
  11. theorem OAI.SK.Analytic.blockPrior_not_self line 61
  12. theorem OAI.SK.Analytic.bank_pool_coverage line 63
  13. theorem OAI.SK.Analytic.bank_pool_no_triple line 98
  14. theorem OAI.SK.Analytic.bank_pool_no_vertex line 111