OAI/RepresentationTheory/UniversalSquare/Band/PathGeometry.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Path Geometry.

  1. def OAI.UniversalTensorSquare.candidatePathCell line 16
  2. def OAI.UniversalTensorSquare.attachmentNE line 21
  3. lemma OAI.UniversalTensorSquare.mem_attachmentNE line 25
  4. lemma OAI.UniversalTensorSquare.attachmentNE_card line 32
  5. lemma OAI.UniversalTensorSquare.candidatePathCell_mem line 43
  6. lemma OAI.UniversalTensorSquare.candidatePathCell_injective line 56
  7. lemma OAI.UniversalTensorSquare.pathCell_not_attachment line 65
  8. lemma OAI.UniversalTensorSquare.attachment_disjoint_transpose line 72
  9. lemma OAI.UniversalTensorSquare.attachmentNE_mem line 81
  10. lemma OAI.UniversalTensorSquare.candidate_band_indices line 88
  11. lemma OAI.UniversalTensorSquare.candidatePathCell_odd line 97
  12. lemma OAI.UniversalTensorSquare.candidatePathCell_even line 105
  13. theorem OAI.UniversalTensorSquare.candidate_band_cell_decomposition line 113
  14. theorem OAI.UniversalTensorSquare.candidate_band_cells line 134
  15. theorem OAI.UniversalTensorSquare.path_endpoint_clearance line 156