OAI/MathematicalPhysics/NavierStokes/ShearFlows/Geometry.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ShearFlows.positiveMinimum line 13
  2. theorem OAI.ShearFlows.positiveMinimum_pos line 15
  3. theorem OAI.ShearFlows.positiveMinimum_le_of_mem line 22
  4. def OAI.ShearFlows.boxGap line 31
  5. theorem OAI.ShearFlows.boxGap_bounds line 36
  6. theorem OAI.ShearFlows.boxGap_pos_of_separated line 44
  7. def OAI.ShearFlows.boxChartGap line 69
  8. theorem OAI.ShearFlows.boxChartGap_bounds line 74
  9. theorem OAI.ShearFlows.boxChartGap_pos line 82
  10. def OAI.ShearFlows.collarRadius line 87
  11. theorem OAI.ShearFlows.collarRadius_pos line 92
  12. theorem OAI.ShearFlows.collarRadius_chart_bound line 111
  13. theorem OAI.ShearFlows.collarRadius_gap_bound line 122
  14. def OAI.ShearFlows.RationalBox.inflate line 140
  15. theorem OAI.ShearFlows.RationalBox.subset_inflate line 144
  16. theorem OAI.ShearFlows.RationalBox.inflate_mono line 151
  17. theorem OAI.ShearFlows.collar_inside_chart line 162
  18. theorem OAI.ShearFlows.collar_disjoint line 170