OAI/Analysis/JiangSu/DimensionDrop/DimensionDropEndpointGenerators.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentMain.ProjectionRow.matrixHom_unit line 19
2. lemma OAI.DimensionDropRelations.Witness.lowerEndpointHom_phi line 32
3. lemma OAI.DimensionDropRelations.Witness.lowerEndpointHom_s line 38
4. lemma OAI.DimensionDropRelations.Witness.upperEndpointHom_phi line 48