OAI/Analysis/SymmetricDomains/ForwardBackwardGerm.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Release061.NashBoundaryChart.reconstruct_oldPosition line 39
  2. def OAI.Release061.NashBoundaryScalingChart.forward line 49
  3. def OAI.Release061.NashBoundaryScalingChart.backward line 53
  4. def OAI.Release061.NashBoundaryScalingChart.HasCutoffs line 57
  5. theorem OAI.Release061.NashBoundaryScalingChart.forward_zero line 63
  6. theorem OAI.Release061.NashBoundaryScalingChart.backward_center line 67
  7. theorem OAI.Release061.NashBoundaryScalingChart.backward_analytic line 71
  8. theorem OAI.Release061.NashBoundaryScalingChart.forward_analytic line 76
  9. theorem OAI.Release061.NashBoundaryScalingChart.backward_forward line 83
  10. theorem OAI.Release061.NashBoundaryScalingChart.forward_mem_variety line 89
  11. theorem OAI.Release061.NashBoundaryScalingChart.family_iff line 93
  12. def OAI.Release061.NashBoundaryScalingChart.domain line 101
  13. theorem OAI.Release061.NashBoundaryScalingChart.domain_eq line 105
  14. theorem OAI.Release061.NashBoundaryScalingChart.forward_backward_germ line 114