OAI/Probability/ClassicalON/SignedSigns.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ClassicalON.bondConnected_refl line 12
  2. theorem OAI.ClassicalON.bondConnected_symm line 15
  3. theorem OAI.ClassicalON.bondConnected_trans line 18
  4. theorem OAI.ClassicalON.bondConnected_endpoints line 22
  5. theorem OAI.ClassicalON.compatibleSigns_connected line 25
  6. def OAI.ClassicalON.prescribedCompatibleSigns line 33
  7. def OAI.ClassicalON.signTranslate line 36
  8. theorem OAI.ClassicalON.signTranslate_compatible line 42
  9. def OAI.ClassicalON.prescribedCompatibleSignsEquiv line 56
  10. theorem OAI.ClassicalON.prescribedCompatibleSigns_card_of_nonempty line 74
  11. def OAI.ClassicalON.bondCrossing line 82
  12. def OAI.ClassicalON.layerSigns line 85
  13. theorem OAI.ClassicalON.layerSigns_consistent_iff line 88
  14. theorem OAI.ClassicalON.layerSigns_card line 123