OAI/Topology/CoarseAssembly/ExplicitCutDown.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The explicit represented-subspace cut-down cycle

  1. theorem OAI.CoarseAssembly.Analytic.representedCorrection_right line 14
  2. theorem OAI.CoarseAssembly.Analytic.representedCorrection_left line 21
  3. theorem OAI.CoarseAssembly.Analytic.representedCorrection_star line 28
  4. theorem OAI.CoarseAssembly.Analytic.OddCycle.cutDown_operator line 35
  5. theorem OAI.CoarseAssembly.Analytic.OddCycle.cutDown_representation line 40
  6. theorem OAI.CoarseAssembly.Analytic.cutDown_class line 43
  7. theorem OAI.CoarseAssembly.Analytic.cutDown_selfAdjoint line 47
  8. theorem OAI.CoarseAssembly.Analytic.cutDown_complement line 51
  9. theorem OAI.CoarseAssembly.Analytic.cutDown_square_compact line 59
  10. theorem OAI.CoarseAssembly.Analytic.symmetricCutDown_square_compact line 63