OAI/Computability/PerfectCompleteness/Construction/DescendantSpacesLemmas.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.PerfectCompleteness.DescendantSpaces.Path line 14
  2. def OAI.PerfectCompleteness.DescendantSpaces.Path.slotEmbedding line 23
  3. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.slotEmbedding_refl line 27
  4. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.slotEmbedding_step line 30
  5. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.slotEmbedding_injective line 34
  6. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.height_le line 42
  7. abbrev OAI.PerfectCompleteness.DescendantSpaces.Path.family line 47
  8. def OAI.PerfectCompleteness.DescendantSpaces.Path.restriction line 50
  9. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.restriction_apply line 53
  10. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.restriction_refl line 57
  11. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.restriction_step line 60
  12. theorem OAI.PerfectCompleteness.DescendantSpaces.Path.restriction_surjective line 65
  13. theorem OAI.PerfectCompleteness.DescendantSpaces.space_descendant_le line 81
  14. theorem OAI.PerfectCompleteness.DescendantSpaces.squareSpace_descendant_le line 100
  15. theorem OAI.PerfectCompleteness.DescendantSpaces.step_square_le_space line 106
  16. theorem OAI.PerfectCompleteness.DescendantSpaces.descendant_square_le_space line 119
  17. theorem OAI.PerfectCompleteness.DescendantSpaces.descendant_pullback_injective line 130
  18. def OAI.PerfectCompleteness.DescendantProducts.lower line 146
  19. theorem OAI.PerfectCompleteness.DescendantProducts.quadraticSpan_le_ancestor line 152
  20. theorem OAI.PerfectCompleteness.DescendantProducts.quadraticSpan_le_displayed line 167
  21. def OAI.PerfectCompleteness.DescendantProducts.ancestorRow line 174