OAI/Geometry/CylinderCovering/Caps/FiniteShape.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CylinderCovering.HalfheightFinite.Shape.height_pos line 12
  2. lemma OAI.CylinderCovering.HalfheightFinite.Shape.foot_eq_affine line 14
  3. def OAI.CylinderCovering.HalfheightFinite.Shape.firstFootLinear line 27
  4. def OAI.CylinderCovering.HalfheightFinite.Shape.secondFootLinear line 32
  5. def OAI.CylinderCovering.HalfheightFinite.Shape.secondFootAffine line 37
  6. def OAI.CylinderCovering.HalfheightFinite.Shape.projectionLinear line 44
  7. lemma OAI.CylinderCovering.HalfheightFinite.Shape.projectionLinear_apply line 47
  8. def OAI.CylinderCovering.HalfheightFinite.Shape.firstProjectedAffine line 50
  9. def OAI.CylinderCovering.HalfheightFinite.Shape.secondProjectedAffine line 53
  10. lemma OAI.CylinderCovering.HalfheightFinite.Shape.firstRaw_ne_zero line 56
  11. lemma OAI.CylinderCovering.HalfheightFinite.Shape.secondRaw_ne_zero line 61
  12. lemma OAI.CylinderCovering.HalfheightFinite.Shape.firstAxis_zero_ne line 66
  13. lemma OAI.CylinderCovering.HalfheightFinite.Shape.secondAxis_one_ne line 69
  14. lemma OAI.CylinderCovering.HalfheightFinite.Shape.projection_injective_on_coordinate_plane line 72
  15. lemma OAI.CylinderCovering.HalfheightFinite.Shape.firstProjectedAffine_injective line 81
  16. lemma OAI.CylinderCovering.HalfheightFinite.Shape.secondProjectedAffine_injective line 95
  17. lemma OAI.CylinderCovering.HalfheightFinite.Shape.firstBase_eq_image line 110
  18. lemma OAI.CylinderCovering.HalfheightFinite.Shape.secondBase_eq_image line 115
  19. def OAI.CylinderCovering.HalfheightFinite.Shape.coordinateVertices line 120
  20. def OAI.CylinderCovering.HalfheightFinite.Shape.firstVertices line 124
  21. def OAI.CylinderCovering.HalfheightFinite.Shape.secondVertices line 127
  22. lemma OAI.CylinderCovering.HalfheightFinite.Shape.halfwidth_pos line 130
  23. lemma OAI.CylinderCovering.HalfheightFinite.Shape.radial_length_pos line 134
  24. lemma OAI.CylinderCovering.HalfheightFinite.Shape.coordinate_shape line 139
  25. theorem OAI.CylinderCovering.HalfheightFinite.Shape.projected_shape line 151
  26. lemma OAI.CylinderCovering.HalfheightFinite.Shape.vertical_triangle_independent line 167
  27. lemma OAI.CylinderCovering.HalfheightFinite.Shape.coordinate_nondegenerate line 181
  28. theorem OAI.CylinderCovering.HalfheightFinite.Shape.projected_nondegenerate line 194
  29. lemma OAI.CylinderCovering.HalfheightFinite.Shape.coordinate_parallel_sides line 211
  30. lemma OAI.CylinderCovering.HalfheightFinite.Shape.affine_side line 219
  31. lemma OAI.CylinderCovering.HalfheightFinite.Shape.affine_vertical_ne_zero line 226
  32. theorem OAI.CylinderCovering.HalfheightFinite.Shape.projected_parallel_sides line 236
  33. theorem OAI.CylinderCovering.HalfheightFinite.Shape.family_shape line 259