OAI/Geometry/CylinderCovering/Physical/SweepTransport.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RadialPhysical.mapToCanonical_injective line 13
  2. lemma OAI.RadialPhysical.mapCenteredToCanonical_injective line 19
  3. lemma OAI.RadialPhysical.halfheight_upperSweep_image line 23
  4. lemma OAI.RadialPhysical.halfheight_lowerSweep_image line 63
  5. lemma OAI.RadialPhysical.centered_upperSweep_image line 103
  6. lemma OAI.RadialPhysical.centered_lowerSweep_image line 143
  7. lemma OAI.RadialPhysical.physical_canonical_tetrahedron line 183
  8. lemma OAI.RadialPhysical.centered_modelBody line 192
  9. theorem OAI.RadialPhysical.halfheight_coverage_of_canonical line 203
  10. theorem OAI.RadialPhysical.centered_coverage_of_canonical line 221
  11. lemma OAI.RadialPhysical.physical_linear_cap_profile line 239
  12. lemma OAI.RadialPhysical.physical_square_cap_profile line 246
  13. lemma OAI.RadialPhysical.centered_linear_cap_profile line 253
  14. theorem OAI.RadialPhysical.halfheight_linear_covers line 260
  15. theorem OAI.RadialPhysical.centered_linear_covers line 269
  16. theorem OAI.RadialPhysical.eventually_halfheight_linear_covers line 278
  17. theorem OAI.RadialPhysical.eventually_centered_linear_covers line 287
  18. theorem OAI.RadialPhysical.eventually_halfheight_square_covers line 296
  19. theorem OAI.RadialPhysical.eventually_centered_square_covers line 308
  20. lemma OAI.RadialPhysical.effectiveTilt_fractional_power line 320
  21. lemma OAI.RadialPhysical.centered_cubic_cap_profile line 328
  22. lemma OAI.RadialPhysical.centered_fractional_cap_profile line 337
  23. theorem OAI.RadialPhysical.centered_cubic_covers line 348
  24. theorem OAI.RadialPhysical.eventually_centered_fractional_covers line 358
  25. theorem OAI.RadialPhysical.halfheight_cubic_covers line 372
  26. theorem OAI.RadialPhysical.eventually_halfheight_fractional_covers line 387