OAI/Probability/CriticalZ3/Symmetry.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CriticalZ3.internalSites line 10
  2. def OAI.CriticalZ3.internalBonds line 11
  3. theorem OAI.CriticalZ3.mem_internalBonds line 14
  4. theorem OAI.CriticalZ3.bondWithin_congr line 18
  5. theorem OAI.CriticalZ3.siteWithin_congr line 38
  6. theorem OAI.CriticalZ3.bondSeedReaches_determined line 48
  7. theorem OAI.CriticalZ3.siteSeedReaches_determined line 54
  8. theorem OAI.CriticalZ3.bondOpen_mono line 65
  9. theorem OAI.CriticalZ3.siteOpen_mono line 71
  10. theorem OAI.CriticalZ3.bondSeedReaches_mono line 75
  11. theorem OAI.CriticalZ3.siteSeedReaches_mono line 82
  12. structure OAI.CriticalZ3.SignedSymmetry line 94
  13. def OAI.CriticalZ3.SignedSymmetry.vertex line 101
  14. def OAI.CriticalZ3.SignedSymmetry.edgeShift line 114
  15. def OAI.CriticalZ3.SignedSymmetry.bond line 117
  16. theorem OAI.CriticalZ3.SignedSymmetry.bond_apply line 122
  17. theorem OAI.CriticalZ3.SignedSymmetry.edge_spec line 125
  18. def OAI.CriticalZ3.SignedSymmetry.Endpoints line 157
  19. theorem OAI.CriticalZ3.SignedSymmetry.endpoints_map line 160
  20. theorem OAI.CriticalZ3.SignedSymmetry.bondOpen_iff line 171
  21. theorem OAI.CriticalZ3.SignedSymmetry.bondOpen_map line 181
  22. theorem OAI.CriticalZ3.SignedSymmetry.neighbor_map line 192
  23. theorem OAI.CriticalZ3.SignedSymmetry.siteOpen_map line 199
  24. theorem OAI.CriticalZ3.SignedSymmetry.cube_map line 203