OAI/Computability/WLIdentification/LeafPresentation.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.WLIdentification.FinitePresentation.PresentedGraph.adjacent_poly_of line 13
  2. def OAI.WLIdentification.FinitePresentation.PresentedGraph.leafAdj line 20
  3. def OAI.WLIdentification.FinitePresentation.PresentedGraph.leaves line 24
  4. def OAI.WLIdentification.FinitePresentation.PresentedGraph.tags line 55
  5. def OAI.WLIdentification.FinitePresentation.PresentedGraph.tagged line 61
  6. theorem OAI.WLIdentification.FinitePresentation.rows_get line 68
  7. def OAI.WLIdentification.FinitePresentation.PresentedGraph.matrix line 85
  8. theorem OAI.WLIdentification.FinitePresentation.PresentedGraph.matrix_eq line 88
  9. theorem OAI.WLIdentification.FinitePresentation.PresentedGraph.matrix_poly line 101
  10. def OAI.WLIdentification.FinitePresentation.PresentedGraph.output line 109
  11. theorem OAI.WLIdentification.FinitePresentation.PresentedGraph.output_eq line 112
  12. theorem OAI.WLIdentification.FinitePresentation.PresentedGraph.output_poly line 115
  13. theorem OAI.WLIdentification.identifies_isomorphic line 123
  14. theorem OAI.WLIdentification.WLdim_isomorphic line 130