OAI/Analysis/HyperbolicCones/TangentFigure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Paper256.exists_smooth_constant_rank_extension line 15
  2. theorem OAI.Paper256.tangentCurve_mem_span line 39
  3. theorem OAI.Paper256.tangentCurve_zero line 46
  4. theorem OAI.Paper256.kernelProjection_zero line 49
  5. theorem OAI.Paper256.kernelProjection_eq_one_of_rank_zero line 53
  6. theorem OAI.Paper256.matrix_independent_spanning_columns line 60
  7. theorem OAI.Paper256.matrix_columns_independent_neighborhood line 78
  8. theorem OAI.Paper256.matrix_columns_span_of_rank_le line 95
  9. theorem OAI.Paper256.matrix_fixed_columns_local_frame line 107