OAI/Geometry/Borsuk/Projectors/NegativeQuadratic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BorsukNine.NegativeQuadratic line 14
  2. lemma OAI.BorsukNine.negativeQuadratic_of_unit line 16
  3. lemma OAI.BorsukNine.negativeQuadratic_isOpen line 25
  4. lemma OAI.BorsukNine.negativeQuadratic_pos_sub line 38
  5. lemma OAI.BorsukNine.matrixEmbed_selfAdjoint line 55
  6. lemma OAI.BorsukNine.matrixCompress_selfAdjoint line 63
  7. lemma OAI.BorsukNine.matrixCompress_embed line 70
  8. lemma OAI.BorsukNine.isometryMatrix_star_action line 78
  9. lemma OAI.BorsukNine.matrixCompress_action line 87
  10. def OAI.BorsukNine.blockScalar line 96
  11. def OAI.BorsukNine.blockOff line 97
  12. def OAI.BorsukNine.blockCorner line 98
  13. lemma OAI.BorsukNine.blockCorner_selfAdjoint line 101
  14. lemma OAI.BorsukNine.blockCorner_kernel line 103
  15. lemma OAI.BorsukNine.blockCorner_of_kernel line 105
  16. lemma OAI.BorsukNine.block_data_zero line 112
  17. lemma OAI.BorsukNine.blockScalar_continuous line 123
  18. lemma OAI.BorsukNine.blockOff_continuous line 126
  19. lemma OAI.BorsukNine.blockCorner_continuous line 130
  20. lemma OAI.BorsukNine.blockOff_eigenvector line 133