OAI/Topology/CoarseAssembly/RelativeTwoByTwo.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Two-by-two relative unitaries for the spatial stabilization argument

  1. def OAI.CoarseAssembly.OperatorKTheory.matrixTwoStarHom line 15
  2. theorem OAI.CoarseAssembly.OperatorKTheory.matrixTwoStarHom_injective line 26
  3. theorem OAI.CoarseAssembly.OperatorKTheory.matrixTwoStarHom_continuous line 33
  4. def OAI.CoarseAssembly.OperatorKTheory.relativeTwoPart line 42
  5. theorem OAI.CoarseAssembly.OperatorKTheory.relativeTwoPart_coe line 49
  6. theorem OAI.CoarseAssembly.OperatorKTheory.relativeTwoPart_star_mul line 53
  7. theorem OAI.CoarseAssembly.OperatorKTheory.relativeTwoPart_mul_star line 63
  8. def OAI.CoarseAssembly.OperatorKTheory.relativeTwoUnitary line 73