OAI/Computability/PerfectCompleteness/Construction/NodeEmbedding.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.NodeEmbedding.NumberedDomain line 19
  2. abbrev OAI.PerfectCompleteness.NodeEmbedding.NodeH line 22
  3. def OAI.PerfectCompleteness.NodeEmbedding.numberedRestriction line 28
  4. theorem OAI.PerfectCompleteness.NodeEmbedding.numberedRestriction_surjective line 31
  5. theorem OAI.PerfectCompleteness.NodeEmbedding.pullback_injective line 34
  6. def OAI.PerfectCompleteness.NodeEmbedding.RowSpace line 38
  7. def OAI.PerfectCompleteness.NodeEmbedding.equiv line 41
  8. def OAI.PerfectCompleteness.NodeEmbedding.embed line 46
  9. theorem OAI.PerfectCompleteness.NodeEmbedding.equiv_apply line 49
  10. theorem OAI.PerfectCompleteness.NodeEmbedding.embed_apply line 52
  11. theorem OAI.PerfectCompleteness.NodeEmbedding.embed_injective line 55
  12. theorem OAI.PerfectCompleteness.NodeEmbedding.embed_surjective line 58
  13. theorem OAI.PerfectCompleteness.NodeEmbedding.finrank_eq line 61
  14. theorem OAI.PerfectCompleteness.NodeEmbedding.card_eq line 65
  15. theorem OAI.PerfectCompleteness.NodeEmbedding.uniform_embed line 68
  16. def OAI.PerfectCompleteness.NodeEmbedding.rowsEquiv line 74
  17. theorem OAI.PerfectCompleteness.NodeEmbedding.rowsEquiv_apply line 78
  18. theorem OAI.PerfectCompleteness.NodeEmbedding.uniform_rowsEquiv line 81
  19. theorem OAI.PerfectCompleteness.NodeEmbedding.squareSpace_eq line 89
  20. theorem OAI.PerfectCompleteness.NodeEmbedding.embed_mul line 96
  21. def OAI.PerfectCompleteness.NodeEmbedding.RootRowSpace line 100
  22. theorem OAI.PerfectCompleteness.NodeEmbedding.rowSpace_le_root line 103
  23. theorem OAI.PerfectCompleteness.NodeEmbedding.squareSpace_le_root line 113
  24. def OAI.PerfectCompleteness.NodeEmbedding.embeddedRows line 128
  25. theorem OAI.PerfectCompleteness.NodeEmbedding.embeddedRows_apply line 132
  26. def OAI.PerfectCompleteness.NodeEmbedding.matrix line 137
  27. theorem OAI.PerfectCompleteness.NodeEmbedding.matrix_evaluate line 141
  28. theorem OAI.PerfectCompleteness.NodeEmbedding.evaluation_comp_embed line 146