OAI/Geometry/CylinderCovering/Physical/UnitEdgeFootprints.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CylinderCovering.UnitEdgeFootprints.e line 15
  2. def OAI.CylinderCovering.UnitEdgeFootprints.a line 16
  3. def OAI.CylinderCovering.UnitEdgeFootprints.b line 17
  4. def OAI.CylinderCovering.UnitEdgeFootprints.velocity line 18
  5. lemma OAI.CylinderCovering.UnitEdgeFootprints.height_pos line 21
  6. lemma OAI.CylinderCovering.UnitEdgeFootprints.height_sq line 22
  7. lemma OAI.CylinderCovering.UnitEdgeFootprints.normal_unit line 24
  8. lemma OAI.CylinderCovering.UnitEdgeFootprints.normal_a line 28
  9. lemma OAI.CylinderCovering.UnitEdgeFootprints.normal_b line 29
  10. lemma OAI.CylinderCovering.UnitEdgeFootprints.normal_velocity line 30
  11. lemma OAI.CylinderCovering.UnitEdgeFootprints.raw_eq line 33
  12. lemma OAI.CylinderCovering.UnitEdgeFootprints.chart_eq line 37
  13. lemma OAI.CylinderCovering.UnitEdgeFootprints.gram_factor line 42
  14. lemma OAI.CylinderCovering.UnitEdgeFootprints.velocity_norm_sq line 49
  15. lemma OAI.CylinderCovering.UnitEdgeFootprints.triangle_eq line 55
  16. theorem OAI.CylinderCovering.UnitEdgeFootprints.local_realization line 66
  17. lemma OAI.CylinderCovering.UnitEdgeFootprints.mesh_eq line 113
  18. lemma OAI.CylinderCovering.UnitEdgeFootprints.midpoint_mem line 116
  19. lemma OAI.CylinderCovering.UnitEdgeFootprints.midpoint_bound line 125
  20. theorem OAI.CylinderCovering.UnitEdgeFootprints.sourceCap_continuous line 133
  21. theorem OAI.CylinderCovering.UnitEdgeFootprints.sourceCap_pos line 137
  22. theorem OAI.CylinderCovering.UnitEdgeFootprints.family_realization line 142