OAI/Computability/PerfectCompleteness/Construction/ProjectedNodeEmbedding.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.ProjectedNodeEmbedding.nativePullback line 20
  2. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.nativePullback_apply line 24
  3. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.nativePullback_injective line 29
  4. def OAI.PerfectCompleteness.ProjectedNodeEmbedding.intoOriginal line 32
  5. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.intoOriginal_injective line 36
  6. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.intoOriginal_apply line 39
  7. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.numberedRestriction_projection line 45
  8. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.intoOriginal_apply_projected line 54
  9. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.intoOriginal_val line 61
  10. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.intoOriginal_at_assignment line 69
  11. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.dualMap_eq_upperTarget line 79
  12. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.evaluation_dualMap line 86
  13. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.intoOriginal_mul line 96
  14. def OAI.PerfectCompleteness.ProjectedNodeEmbedding.intoOriginalSquare line 102
  15. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.intoOriginalSquare_apply line 112
  16. theorem OAI.PerfectCompleteness.ProjectedNodeEmbedding.intoOriginalSquare_product line 119