OAI/Topology/CoarseAssembly/LocallyCompactAlgebra.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Local compactness of every operator in the reduced Roe algebra

  1. theorem OAI.CoarseAssembly.DiscreteRoe.locallyCompact_zero line 23
  2. theorem OAI.CoarseAssembly.DiscreteRoe.LocallyCompact.add line 29
  3. theorem OAI.CoarseAssembly.DiscreteRoe.LocallyCompact.mul line 36
  4. theorem OAI.CoarseAssembly.DiscreteRoe.LocallyCompact.smul line 46
  5. theorem OAI.CoarseAssembly.DiscreteRoe.locallyCompact_closed line 53
  6. def OAI.CoarseAssembly.DiscreteRoe.locallyCompactAlgebra line 60
  7. theorem OAI.CoarseAssembly.DiscreteRoe.operator_star_continuous line 72
  8. theorem OAI.CoarseAssembly.DiscreteRoe.locallyCompactAlgebra_closed line 76
  9. theorem OAI.CoarseAssembly.DiscreteRoe.roe_locallyCompact line 82