OAI/Analysis/SymmetricDomains/SliceGraphDerivativeBound.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Release061.normalParameterInjection line 35
  2. lemma OAI.Release061.normalParameterInjection_norm_le line 48
  3. lemma OAI.Release061.normalParameterInjection_opNorm line 57
  4. lemma OAI.Release061.complexGraphRealEquiv_normal line 62
  5. lemma OAI.Release061.ProjectionNashChart.coordinateDomain_isOpen line 72
  6. def OAI.Release061.NashBoundaryChart.normalInjection line 101
  7. def OAI.Release061.NashBoundaryChart.sliceLift line 106
  8. def OAI.Release061.NashBoundaryChart.sliceParameter line 111
  9. def OAI.Release061.NashBoundaryChart.sliceGraph line 116
  10. def OAI.Release061.NashBoundaryChart.sliceDomain line 121
  11. lemma OAI.Release061.NashBoundaryChart.sliceLift_analytic line 125
  12. lemma OAI.Release061.NashBoundaryChart.sliceParameter_zero line 130
  13. lemma OAI.Release061.NashBoundaryChart.sliceGraph_zero line 133
  14. lemma OAI.Release061.NashBoundaryChart.slice_real_coordinates line 136
  15. lemma OAI.Release061.NashBoundaryChart.sliceDomain_isOpen line 149
  16. lemma OAI.Release061.NashBoundaryChart.sliceGraph_analytic line 154
  17. lemma OAI.Release061.NashBoundaryChart.sliceGraph_derivative_bound line 163