OAI/Topology/CoarseAssembly/LocalCompactPerturbation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Locally compact changes of Fredholm operators

This also permits changing an operator on the subspace where its representation vanishes. Compactness is required only after multiplying by a represented coefficient.

  1. theorem OAI.CoarseAssembly.Analytic.compact_local_smul_right line 19
  2. theorem OAI.CoarseAssembly.Analytic.compact_local_smul_left line 25
  3. theorem OAI.CoarseAssembly.Analytic.compact_local_smul_star line 31
  4. def OAI.CoarseAssembly.Analytic.OddCycle.localCompactHomotopy line 37
  5. theorem OAI.CoarseAssembly.Analytic.localCompactPerturb_class line 56