include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
include ☞http://mathhub.info/MitM/core/geometry?Planes ❙
include ?FrameITBasics ❙
include ?FrameITCircle ❙
cylinderType : type ❘ # Cylinder ❙
cylinderCons : circle ⟶ point ⟶ Cylinder ❘ # CylinderCons 1 2 ❙
// takes a midpoint, a point on the edge of the base-circle plane, as well as a point in the base-circle plane, and a point directly above the midpoint ❙
cylinderCons : point ⟶ point ⟶ point ⟶ point ⟶ Cylinder ❘ # CylinderCons 1 2 3 4 ❙
meta ?MetaAnnotations?problemTheory ?CylinderScroll/Problem ❙
meta ?MetaAnnotations?solutionTheory ?CylinderScroll/Solution ❙
theory Problem =
M: point
❘ meta ?MetaAnnotations?label "M"
❘ meta ?MetaAnnotations?description "The point in the middle of the bottom circle-plane"
❙
E: point
❘ meta ?MetaAnnotations?label "E"
❘ meta ?MetaAnnotations?description "The point on the edge of the bottom-circle-plane"
❙
P: point
❘ meta ?MetaAnnotations?label "P"
❘ meta ?MetaAnnotations?description "A point in the bottom-circle-plane"
❙
T: point
❘ meta ?MetaAnnotations?label "T"
❘ meta ?MetaAnnotations?description "The point directly above the point M"
❙
❚
theory Solution =
include ?CylinderScroll/Problem ❙
meta ?MetaAnnotations?label "Cylinder" ❙
meta ?MetaAnnotations?description s"Given four points: Three points that form the bottom-plane and one directly above this scroll constructs a cylinder" ❙
ConstructedCylinder: Cylinder
❘ = ( CylinderCons M E P T )
❘ meta ?MetaAnnotations?label s"Cylinder"
❘ meta ?MetaAnnotations?description s"The constructed Cylinder."