OAI/Topology/CoarseAssembly/ComponentHilbertInclusion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Componentwise and whole-union spatial inclusions agree

  1. theorem OAI.CoarseAssembly.DiscreteRoe.componentEmbedding_range line 19
  2. theorem OAI.CoarseAssembly.DiscreteRoe.row_inclusion_adjoint line 32
  3. theorem OAI.CoarseAssembly.DiscreteRoe.row_inclusion line 44
  4. theorem OAI.CoarseAssembly.DiscreteRoe.row_isometricExtension line 62