OAI/Analysis/FactorGeneration/ProjectionComparison.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A nonzero coefficient linking two projections produces an actual nonzero partial isometry between subprojections. Scalar center supplies such coefficients.

  1. theorem OAI.Generator.Tracial.exists_partialIsometry_of_link line 18
  2. theorem OAI.Generator.Tracial.exists_nonzero_partialIsometry_between_projections line 34
  3. theorem OAI.Generator.Tracial.exists_partialIsometry_comparison line 70
  4. theorem OAI.Generator.Tracial.projection_eq_of_le_of_trace_eq line 120
  5. theorem OAI.Generator.Tracial.exists_partialIsometry_of_trace_eq line 134