OAI/Computability/PerfectCompleteness/Foundations/SourceProjectedChoices.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceProjectedChoices.Positions line 18
  2. abbrev OAI.PerfectCompleteness.SourceProjectedChoices.Choices line 21
  3. def OAI.PerfectCompleteness.SourceProjectedChoices.tagEquiv line 25
  4. def OAI.PerfectCompleteness.SourceProjectedChoices.choiceLaw line 32
  5. theorem OAI.PerfectCompleteness.SourceProjectedChoices.tagEquiv_law line 36
  6. theorem OAI.PerfectCompleteness.SourceProjectedChoices.choicesLaw_tagEquiv line 50
  7. theorem OAI.PerfectCompleteness.SourceProjectedChoices.tagLaw_choices line 58
  8. def OAI.PerfectCompleteness.SourceProjectedChoices.projected line 70
  9. def OAI.PerfectCompleteness.SourceProjectedChoices.projection line 75
  10. theorem OAI.PerfectCompleteness.SourceProjectedChoices.childDomain_eq line 81
  11. theorem OAI.PerfectCompleteness.SourceProjectedChoices.childProjection_heq line 88
  12. theorem OAI.PerfectCompleteness.SourceProjectedChoices.selectedSlots_tag line 97
  13. theorem OAI.PerfectCompleteness.SourceProjectedChoices.projection_family_heq line 104
  14. theorem OAI.PerfectCompleteness.SourceProjectedChoices.selectedProjection_tag line 115
  15. theorem OAI.PerfectCompleteness.SourceProjectedChoices.selectedSlots_source line 129
  16. theorem OAI.PerfectCompleteness.SourceProjectedChoices.selectedProjection_source line 137