OAI/Computability/WLIdentification/AffinePresentation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WLIdentification.FinitePresentation.Presented.bit line 9
  2. theorem OAI.WLIdentification.FinitePresentation.Presented.bit_code line 12
  3. def OAI.WLIdentification.FinitePresentation.affineLocals line 17
  4. structure OAI.WLIdentification.FinitePresentation.AffineRealizer line 23
  5. abbrev OAI.WLIdentification.FinitePresentation.AffineRealizer.localData line 32
  6. def OAI.WLIdentification.FinitePresentation.AffineRealizer.legalEquiv line 34
  7. def OAI.WLIdentification.FinitePresentation.AffineRealizer.legalPoints line 41
  8. def OAI.WLIdentification.FinitePresentation.AffineRealizer.vertices line 44
  9. theorem OAI.WLIdentification.FinitePresentation.AffineRealizer.legalPoints_code line 47
  10. theorem OAI.WLIdentification.FinitePresentation.AffineRealizer.vertices_code_inl line 50
  11. theorem OAI.WLIdentification.FinitePresentation.AffineRealizer.vertices_code_inr line 53
  12. def OAI.WLIdentification.FinitePresentation.AffineRealizer.cross line 56
  13. theorem OAI.WLIdentification.FinitePresentation.AffineRealizer.cross_correct line 60
  14. theorem OAI.WLIdentification.FinitePresentation.AffineRealizer.cross_poly line 78
  15. theorem OAI.WLIdentification.FinitePresentation.AffineRealizer.odd_half line 85
  16. def OAI.WLIdentification.FinitePresentation.AffineRealizer.adjacent line 87
  17. def OAI.WLIdentification.FinitePresentation.AffineRealizer.base line 91
  18. def OAI.WLIdentification.FinitePresentation.AffineRealizer.colors line 119
  19. def OAI.WLIdentification.FinitePresentation.AffineRealizer.uncolored line 136
  20. theorem OAI.WLIdentification.FinitePresentation.AffineRealizer.uncolored_isomorphic line 138