OAI/Analysis/Commutator/FactorComparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.PartialIsometryOrder.Link.residual_source_projection line 23
  2. lemma OAI.Kadison.PartialIsometryOrder.Link.residual_target_projection line 28
  3. lemma OAI.Kadison.PartialIsometryOrder.Link.residual_mul_initial line 33
  4. lemma OAI.Kadison.PartialIsometryOrder.Link.final_mul_residual line 41
  5. lemma OAI.Kadison.PartialIsometryOrder.Link.residual_cross line 49
  6. def OAI.Kadison.PartialIsometryOrder.Link.extend line 64
  7. lemma OAI.Kadison.PartialIsometryOrder.Link.extend_val line 90
  8. lemma OAI.Kadison.PartialIsometryOrder.Link.le_extend line 93
  9. theorem OAI.Kadison.PartialIsometryOrder.factor_comparison line 107