OAI/Computability/WLIdentification/LocalPresentation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.WLIdentification.FinitePresentation.Locals line 10
  2. abbrev OAI.WLIdentification.FinitePresentation.Locals.Value line 18
  3. def OAI.WLIdentification.FinitePresentation.Locals.good line 20
  4. theorem OAI.WLIdentification.FinitePresentation.Locals.good_iff line 22
  5. def OAI.WLIdentification.FinitePresentation.Locals.localP line 38
  6. def OAI.WLIdentification.FinitePresentation.Locals.count line 42
  7. theorem OAI.WLIdentification.FinitePresentation.Locals.count_eq line 44
  8. def OAI.WLIdentification.FinitePresentation.Locals.rank line 48
  9. def OAI.WLIdentification.FinitePresentation.Locals.valueEquiv line 50
  10. def OAI.WLIdentification.FinitePresentation.Locals.valueCode line 54
  11. def OAI.WLIdentification.FinitePresentation.Locals.valueGood line 57
  12. theorem OAI.WLIdentification.FinitePresentation.Locals.valueGood_iff line 59
  13. theorem OAI.WLIdentification.FinitePresentation.Locals.good_poly line 68
  14. theorem OAI.WLIdentification.FinitePresentation.Locals.count_poly line 72
  15. theorem OAI.WLIdentification.FinitePresentation.Locals.rank_poly line 80
  16. def OAI.WLIdentification.FinitePresentation.Locals.values line 88
  17. def OAI.WLIdentification.FinitePresentation.Locals.read line 98
  18. theorem OAI.WLIdentification.FinitePresentation.Locals.read_value line 100
  19. theorem OAI.WLIdentification.FinitePresentation.Locals.read_poly line 106