OAI/Analysis/JiangSu/DimensionDrop/EndpointRegrouping.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.JiangSuConstruction.connectingAmbient_injectiveline 17 - lemma
OAI.JiangSuConstruction.connectingMap_injectiveline 24