OAI/Computability/PerfectCompleteness/Foundations/SourceProjectedTag.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.SourceProjectedTag.Flags line 18
  2. abbrev OAI.PerfectCompleteness.SourceProjectedTag.Tag line 20
  3. def OAI.PerfectCompleteness.SourceProjectedTag.positionLaw line 24
  4. def OAI.PerfectCompleteness.SourceProjectedTag.flagLaw line 30
  5. def OAI.PerfectCompleteness.SourceProjectedTag.law line 34
  6. def OAI.PerfectCompleteness.SourceProjectedTag.sourceFlagEquiv line 38
  7. theorem OAI.PerfectCompleteness.SourceProjectedTag.sourceFlagEquiv_apply line 46
  8. theorem OAI.PerfectCompleteness.SourceProjectedTag.sourceFlagEquiv_symm_apply line 53
  9. theorem OAI.PerfectCompleteness.SourceProjectedTag.sourceFlagEquiv_law line 59
  10. def OAI.PerfectCompleteness.SourceProjectedTag.originalSlots line 79
  11. theorem OAI.PerfectCompleteness.SourceProjectedTag.parentLeftSlots_sources line 82
  12. def OAI.PerfectCompleteness.SourceProjectedTag.mixedInside line 90
  13. def OAI.PerfectCompleteness.SourceProjectedTag.projection line 94