OAI/Topology/CoarseAssembly/RelativeTwoHomotopy.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Relative two-by-two classes and their actual norm homotopies

  1. def OAI.CoarseAssembly.OperatorKTheory.relativeTwoMatrix line 16
  2. theorem OAI.CoarseAssembly.OperatorKTheory.relativeTwoMatrix_scalar line 21
  3. def OAI.CoarseAssembly.OperatorKTheory.relativeTwoClass line 32
  4. theorem OAI.CoarseAssembly.OperatorKTheory.continuous_relativeTwoUnitary line 40
  5. theorem OAI.CoarseAssembly.OperatorKTheory.continuous_relativeTwoMatrix line 53
  6. theorem OAI.CoarseAssembly.OperatorKTheory.relativeTwoClass_homotopy line 61