OAI/Analysis/JiangSu/DimensionDrop/DimensionDropSurgeryConnected.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.JiangSuConstruction.left_le_dropFiber line 15
  2. lemma OAI.JiangSuConstruction.right_le_dropFiber line 20
  3. lemma OAI.JiangSuConstruction.pFlow_mem_drop line 27
  4. lemma OAI.JiangSuConstruction.qFlow_mem_drop line 35
  5. lemma OAI.JiangSuConstruction.squareUnitary_continuous line 44
  6. def OAI.JiangSuConstruction.residualSection line 58
  7. lemma OAI.JiangSuConstruction.residualSection_mem line 66
  8. def OAI.JiangSuConstruction.residualUnitary line 75
  9. lemma OAI.JiangSuConstruction.residualUnitary_continuous line 78
  10. lemma OAI.JiangSuConstruction.residualUnitary_zero line 87
  11. lemma OAI.JiangSuConstruction.residualUnitary_one line 95
  12. def OAI.JiangSuConstruction.contractInterval line 110
  13. lemma OAI.JiangSuConstruction.contractInterval_continuous line 113
  14. lemma OAI.JiangSuConstruction.contractInterval_zero line 116
  15. lemma OAI.JiangSuConstruction.contractInterval_one line 118
  16. def OAI.JiangSuConstruction.contractedMatching line 122
  17. lemma OAI.JiangSuConstruction.contractedMatching_diag line 128
  18. def OAI.JiangSuConstruction.contractedSurgery line 130
  19. lemma OAI.JiangSuConstruction.contractedSurgery_continuous line 134
  20. lemma OAI.JiangSuConstruction.contractedSurgery_zero line 163
  21. lemma OAI.JiangSuConstruction.contractedSurgery_one line 171
  22. theorem OAI.JiangSuConstruction.surgeryUnitary_joined line 180