OAI/Topology/CoarseAssembly/InvolutionUnitaryPath.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

An explicit path from the identity to a self-adjoint involution

  1. def OAI.CoarseAssembly.Analytic.involutionNegativeProjection line 13
  2. theorem OAI.CoarseAssembly.Analytic.involutionNegativeProjection_isStarProjection line 15
  3. def OAI.CoarseAssembly.Analytic.involutionUnitaryPath line 31
  4. theorem OAI.CoarseAssembly.Analytic.involutionUnitaryPath_continuous line 36
  5. theorem OAI.CoarseAssembly.Analytic.involutionUnitaryPath_start line 40
  6. theorem OAI.CoarseAssembly.Analytic.involutionUnitaryPath_finish line 43