OAI/Topology/CoarseAssembly/IsometricDecomposition.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Extending an orthogonal decomposition by the identity

  1. theorem OAI.CoarseAssembly.isometricExtension_decomposition line 17
  2. theorem OAI.CoarseAssembly.isometry_comp_orthogonal line 41