OAI/Analysis/SegmentLenses/Subspaces.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Primal isometries and coordinate completions

  1. def OAI.SegmentLenses.SegmentEmbedding.testRestriction line 22
  2. theorem OAI.SegmentLenses.SegmentEmbedding.testRestriction_apply line 27
  3. theorem OAI.SegmentLenses.SegmentEmbedding.testRestriction_testMap line 33
  4. theorem OAI.SegmentLenses.SegmentEmbedding.testMap_testRestriction line 39
  5. theorem OAI.SegmentLenses.SegmentEmbedding.norm_testRestriction_le line 52
  6. def OAI.SegmentLenses.SegmentEmbedding.primalRestriction line 80
  7. theorem OAI.SegmentLenses.SegmentEmbedding.primalRestriction_test line 85
  8. theorem OAI.SegmentLenses.SegmentEmbedding.primalRestriction_primalMap line 90
  9. theorem OAI.SegmentLenses.SegmentEmbedding.norm_primalRestriction_le line 97
  10. def OAI.SegmentLenses.completionIsometry line 113
  11. theorem OAI.SegmentLenses.completionIsometry_coe line 123
  12. theorem OAI.SegmentLenses.closureInclusion_dense line 136
  13. def OAI.SegmentLenses.completionClosureEquiv line 147
  14. theorem OAI.SegmentLenses.completionClosureEquiv_coe line 158
  15. abbrev OAI.SegmentLenses.FiniteCoordinates line 172
  16. def OAI.SegmentLenses.coordinateCompletionEquiv line 186
  17. theorem OAI.SegmentLenses.coordinateCompletionEquiv_coe line 189
  18. theorem OAI.SegmentLenses.polar_norm line 197