OAI/Geometry/CubicTorus/Reflection/AxialSectionCorner.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.planarAxialField_admissible line 13
  2. lemma OAI.CubicTorus.planeDivergence_planarAxialField line 25
  3. lemma OAI.CubicTorus.planarAxialField_flux line 35
  4. theorem OAI.CubicTorus.planarTorusPerimeter_ge_axial_flux line 47
  5. lemma OAI.CubicTorus.circlePeriodize_integral_short line 67
  6. theorem OAI.CubicTorus.planarTorusPerimeter_ge_two_of_bump_strips line 84
  7. lemma OAI.CubicTorus.planar_open_fiber_collar line 185
  8. theorem OAI.CubicTorus.planarTorusPerimeter_ge_two_of_open_fibers line 202
  9. def OAI.CubicTorus.axialSectionCorner line 257
  10. lemma OAI.CubicTorus.axialSectionCorner_same line 260
  11. lemma OAI.CubicTorus.axialSectionCorner_other line 262
  12. lemma OAI.CubicTorus.axialSectionCorner_mem line 266
  13. lemma OAI.CubicTorus.octantHeight_zero_le line 274
  14. lemma OAI.CubicTorus.octantHeight_le_one line 279
  15. lemma OAI.CubicTorus.torusAxialSplit_symm_continuous line 284
  16. lemma OAI.CubicTorus.axialSlice_isOpen line 295
  17. lemma OAI.CubicTorus.axialSlice_closure_subset line 299
  18. lemma OAI.CubicTorus.upperFold_closure_mem line 306
  19. lemma OAI.CubicTorus.upperFold_slice_fixed line 314
  20. lemma OAI.CubicTorus.isMinimizerAt_section_full_fiber line 321
  21. lemma OAI.CubicTorus.isMinimizerAt_section_empty_closed_fiber line 351
  22. theorem OAI.CubicTorus.isMinimizerAt_section_strip_perimeter line 383
  23. def OAI.CubicTorus.planarProductField line 422
  24. lemma OAI.CubicTorus.planarProductField_admissible line 426
  25. lemma OAI.CubicTorus.planeDivergence_planarProductField line 454
  26. theorem OAI.CubicTorus.planarTorusPerimeter_ge_product_flux line 468
  27. lemma OAI.CubicTorus.transverse_integral_mul line 506
  28. theorem OAI.CubicTorus.planarTorusPerimeter_ge_weighted_bump_strips line 512
  29. lemma OAI.CubicTorus.planar_open_partial_fiber_collar line 651
  30. theorem OAI.CubicTorus.planarTorusPerimeter_ge_corner_calibration line 670
  31. lemma OAI.CubicTorus.circlePeriodize_abs_lt_one line 724
  32. theorem OAI.CubicTorus.exists_planar_affine_band_field line 744
  33. def OAI.CubicTorus.closedCentralArc line 829
  34. lemma OAI.CubicTorus.closedCentralArc_isCompact line 831