OAI/Topology/CoarseAssembly/IsometryUnitary.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Identity extension of a unitary along an isometry

  1. def OAI.CoarseAssembly.Analytic.isometryCornerHom line 14
  2. def OAI.CoarseAssembly.Analytic.isometryExtensionUnitary line 26
  3. theorem OAI.CoarseAssembly.Analytic.isometryExtensionUnitary_val line 61
  4. theorem OAI.CoarseAssembly.Analytic.isometryDilation_conjugates_unitary line 66