OAI/Topology/CoarseAssembly/RegularizedCycle.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit norm-one representatives compatible with analytic homotopies

  1. theorem OAI.CoarseAssembly.Analytic.OddCycle.regularize_class line 14
  2. theorem OAI.CoarseAssembly.Analytic.OddCycle.regularize_unital line 19
  3. theorem OAI.CoarseAssembly.Analytic.OddCycle.regularize_selfAdjoint line 22
  4. theorem OAI.CoarseAssembly.Analytic.OddCycle.regularize_norm_le line 25
  5. def OAI.CoarseAssembly.Analytic.OddHomotopy.regularize line 28
  6. theorem OAI.CoarseAssembly.Analytic.OddHomotopy.regularize_eval line 33