OAI/Analysis/CircleDomains/Selection/CountableTagAssembly.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Put countably many tag lists into one list without losing any tag. Unused code slots are inactive, so tuple exclusions are preserved exactly.

  1. def OAI.CircleDomainRigidity.assembleTags line 15
  2. theorem OAI.CircleDomainRigidity.assembleTags_at line 20
  3. theorem OAI.CircleDomainRigidity.assembleTags_value line 24
  4. theorem OAI.CircleDomainRigidity.tagRules_assemble line 33
  5. theorem OAI.CircleDomainRigidity.residualTimes_assemble_iff line 49
  6. theorem OAI.CircleDomainRigidity.residualTimes_assemble_on_piece line 67