OAI/Topology/CoarseAssembly/CayleyIntertwining.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The rational boundary respects bounded intertwiners

This includes restriction to a component of a Hilbert direct sum. No multiplicativity of compression on arbitrary operators is assumed.

  1. theorem OAI.CoarseAssembly.Analytic.cayleyDenominator_intertwines line 20
  2. theorem OAI.CoarseAssembly.Analytic.cayleyDenominator_inv_intertwines line 29
  3. theorem OAI.CoarseAssembly.Analytic.cayleyUnitary_intertwines line 49
  4. theorem OAI.CoarseAssembly.Analytic.rationalBoundaryUnitary_intertwines line 59