OAI/Probability/ClassicalON/AnnulusLabels.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ClassicalON.SeparatedCenters line 13
  2. def OAI.ClassicalON.centerLabel line 15
  3. def OAI.ClassicalON.centerPins line 18
  4. theorem OAI.ClassicalON.annulus_unique line 20
  5. theorem OAI.ClassicalON.centerLabel_some_iff line 25
  6. theorem OAI.ClassicalON.centerLabel_none_iff line 40
  7. theorem OAI.ClassicalON.annulusBoundary_subset line 51
  8. theorem OAI.ClassicalON.local_centerPins_iff line 58
  9. def OAI.ClassicalON.LatticeGraph.annulusVertexLabel line 69
  10. def OAI.ClassicalON.LatticeGraph.annulusEdgeLabel line 72
  11. def OAI.ClassicalON.LatticeGraph.allAnnulusPins line 75
  12. theorem OAI.ClassicalON.LatticeGraph.annulusEdgeLabel_some_iff line 78
  13. theorem OAI.ClassicalON.LatticeGraph.annulus_vertex_edge_label line 94
  14. theorem OAI.ClassicalON.LatticeGraph.annulus_left_label line 125
  15. theorem OAI.ClassicalON.LatticeGraph.annulus_right_label line 130