OAI/Topology/CoarseAssembly/ContinuousUnitalization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A path-compatible unital self-adjoint representative

  1. theorem OAI.CoarseAssembly.Analytic.OddCycle.unitalSelfAdjoint_unital line 15
  2. theorem OAI.CoarseAssembly.Analytic.OddCycle.unitalSelfAdjoint_selfAdjoint line 20
  3. theorem OAI.CoarseAssembly.Analytic.OddCycle.unitalSelfAdjoint_class line 23
  4. theorem OAI.CoarseAssembly.Analytic.OddCycle.unitalSelfAdjoint_operator line 28
  5. theorem OAI.CoarseAssembly.Analytic.OddCycle.unitalSelfAdjoint_representation line 32
  6. theorem OAI.CoarseAssembly.Analytic.continuous_symmetricCutDown line 38
  7. def OAI.CoarseAssembly.Analytic.OddHomotopy.unitalSelfAdjoint line 44
  8. theorem OAI.CoarseAssembly.Analytic.OddHomotopy.unitalSelfAdjoint_eval line 62