OAI/Analysis/WeakInfiniteness/TensorInjectivity.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.SpatialRepresentation.precompLeft line 28
  2. def OAI.WeakPureInfiniteness.spatialMapLeft line 35
  3. lemma OAI.WeakPureInfiniteness.spatialMapLeft_elementary line 45
  4. lemma OAI.WeakPureInfiniteness.spatialMapLeft_mem line 48
  5. def OAI.WeakPureInfiniteness.minimalMapLeft line 60
  6. lemma OAI.WeakPureInfiniteness.minimalMapLeft_elementary line 65
  7. lemma OAI.WeakPureInfiniteness.spatialSum_apply line 68
  8. lemma OAI.WeakPureInfiniteness.norm_spatialSum_le_image line 81
  9. lemma OAI.WeakPureInfiniteness.norm_spatialSum_le_image_finset line 103
  10. lemma OAI.WeakPureInfiniteness.norm_spatialMapLeft_ge_on_span line 114
  11. lemma OAI.WeakPureInfiniteness.norm_minimalMapLeft line 126
  12. lemma OAI.WeakPureInfiniteness.minimalMapLeft_isometry line 139