OAI/Topology/CoarseAssembly/IsometricExtension.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Extending a Fredholm operator by the identity off an isometric image

  1. theorem OAI.CoarseAssembly.isometricExtension_selfAdjoint line 16
  2. theorem OAI.CoarseAssembly.isometricExtension_square_defect line 22
  3. theorem OAI.CoarseAssembly.isometricExtension_square_compact line 36
  4. theorem OAI.CoarseAssembly.operatorConjugation_norm_le line 43
  5. theorem OAI.CoarseAssembly.isometricExtension_norm_le line 60