OAI/Analysis/OperatorAlgebra/GNSCornerRange.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Range criteria for a GNS inclusion with a normalized vector formula.

  1. lemma OAI.WeakPureInfiniteness.normalizedCornerGNSInclusion_gnsVector line 13
  2. lemma OAI.WeakPureInfiniteness.gnsInclusion_fixed_of_vectors line 24
  3. lemma OAI.WeakPureInfiniteness.gnsInclusion_range_of_dense_vectors line 34
  4. lemma OAI.WeakPureInfiniteness.isometricCornerProjection_eq_of_range line 45