OAI/Topology/CoarseAssembly/ScalarCutDown.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Cutting a scalar Fredholm operator down to its represented subspace

  1. theorem OAI.CoarseAssembly.Analytic.symmetricCutDown_selfAdjoint line 15
  2. theorem OAI.CoarseAssembly.Analytic.symmetricCutDown_complement line 22
  3. theorem OAI.CoarseAssembly.Analytic.scalar_projection_selfAdjoint line 35
  4. theorem OAI.CoarseAssembly.Analytic.scalar_projection_sq line 39
  5. theorem OAI.CoarseAssembly.Analytic.symmetricCutDown_sub_mul line 42
  6. theorem OAI.CoarseAssembly.Analytic.mul_symmetricCutDown_sub line 50
  7. theorem OAI.CoarseAssembly.Analytic.scalarCutDown_compact line 58
  8. theorem OAI.CoarseAssembly.Analytic.exists_supported_scalar_representative line 86
  9. theorem OAI.CoarseAssembly.Analytic.supported_square_compact line 111