OAI/Topology/CoarseAssembly/PartialIsometryDilation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Swapping two isometric images by a partial-isometry dilation

  1. def OAI.CoarseAssembly.Analytic.partialIsometryDilation line 13
  2. theorem OAI.CoarseAssembly.Analytic.partialIsometryDilation_selfAdjoint line 16
  3. theorem OAI.CoarseAssembly.Analytic.partialIsometry_star_relation line 21
  4. theorem OAI.CoarseAssembly.Analytic.partialIsometry_complement_relations line 26
  5. theorem OAI.CoarseAssembly.Analytic.partialIsometryDilation_sq line 48
  6. def OAI.CoarseAssembly.Analytic.partialIsometryDilationPath line 66

    Source documentation

    A continuous path from one to the symmetry exchanging the two images.

    def partialIsometryDilationPath (T : A) (hT : T * star T * T = T) :
    Interval → unitary (Matrix (Fin 2) (Fin 2) A) :=
…

    Mentions: OAI.CoarseAssembly.Analytic.Interval

  7. theorem OAI.CoarseAssembly.Analytic.partialIsometryDilationPath_continuous line 71
  8. theorem OAI.CoarseAssembly.Analytic.partialIsometryDilationPath_start line 74
  9. theorem OAI.CoarseAssembly.Analytic.partialIsometryDilationPath_finish line 77
  10. theorem OAI.CoarseAssembly.Analytic.partialIsometryDilation_conjugation line 81