OAI/Computability/PerfectCompleteness/Construction/RelativeDescendantProductsLemmas.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PerfectCompleteness.RelativeDescendantProducts.Below line 13
  2. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.Below.height_lt line 21
  3. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.Below.ne line 27
  4. def OAI.PerfectCompleteness.RelativeDescendantProducts.relativeNode line 34
  5. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.relativeNode_height line 40
  6. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.relativeNode_injective line 52
  7. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.relativeNode_below line 65
  8. abbrev OAI.PerfectCompleteness.RelativeDescendantProducts.RelativeDescendant line 82
  9. def OAI.PerfectCompleteness.RelativeDescendantProducts.descendantIndex line 85
  10. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.descendantIndex_below line 89
  11. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.descendantIndex_injective line 94
  12. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.pullback_square_exists line 101
  13. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.squareSpace_le_rowSpace line 130
  14. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.one_mem_rowSpace line 144
  15. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.knownSpace_le_rowSpace line 154
  16. theorem OAI.PerfectCompleteness.RelativeDescendantProducts.relative_knownSpace_le_rowSpace line 177
  17. theorem OAI.PerfectCompleteness.GeometricDescendants.below_nodeAtLevel line 200
  18. def OAI.PerfectCompleteness.GeometricDescendants.lowerLevel line 227
  19. theorem OAI.PerfectCompleteness.GeometricDescendants.lowerLevel_lt line 230
  20. theorem OAI.PerfectCompleteness.GeometricDescendants.lowerLevel_injective line 233
  21. def OAI.PerfectCompleteness.GeometricDescendants.pathDescendant line 238
  22. theorem OAI.PerfectCompleteness.GeometricDescendants.pathDescendant_below line 244
  23. theorem OAI.PerfectCompleteness.GeometricDescendants.pathDescendant_injective line 249
  24. theorem OAI.PerfectCompleteness.GeometricDescendants.knownSpace_le_rowSpace line 261
  25. theorem OAI.PerfectCompleteness.GeometricDescendants.knownSpace_le_factoringSpace line 274