OAI/Analysis/InterpolatedFactors/Restriction.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.FullReducingCorner.transport line 14
  2. theorem OAI.FreeGroupFactorMain.FullReducingCorner.representation_compress line 33
  3. def OAI.FreeGroupFactorMain.FullReducingCorner.reductionImage line 41
  4. theorem OAI.FreeGroupFactorMain.FullReducingCorner.representation_compressedSet line 43
  5. def OAI.FreeGroupFactorMain.FullReducingCorner.restrictionIso line 53
  6. theorem OAI.FreeGroupFactorMain.FullReducingCorner.restrictionIso_apply line 57
  7. def OAI.FreeGroupFactorMain.FullReducingCorner.operatorTopology line 61
  8. theorem OAI.FreeGroupFactorMain.FullReducingCorner.restrictionIso_normal line 65
  9. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.normalHull_projection_mem line 86
  10. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.reduced_generators line 98
  11. def OAI.FreeGroupFactorMain.GaussianRecognition.System.fullReductionIso line 115
  12. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.fullReductionIso_apply line 120
  13. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.fullReductionIso_normal line 124
  14. theorem OAI.FreeGroupFactorMain.GaussianRecognition.System.fullReductionIso_trace line 139
  15. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedFull_left line 152
  16. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedFull_right line 157
  17. theorem OAI.FreeGroupFactorMain.WeightedFock.weightedFull_initial line 162
  18. def OAI.FreeGroupFactorMain.WeightedFock.fullGaussianIso line 167
  19. theorem OAI.FreeGroupFactorMain.WeightedFock.fullGaussianIso_normal line 174
  20. theorem OAI.FreeGroupFactorMain.WeightedFock.fullGaussianIso_trace line 187