CylinderScroll.mmt

namespace http://mathhub.info/FrameIT/frameworld ❚
fixmeta ?FrameworldMeta ❚


theory CylinderScroll =
    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"
        ❙
        T: point
         ❘ meta ?MetaAnnotations?label "T"
         ❘ meta ?MetaAnnotations?description "The point directly above the point M"
        ❙

        dME: Σ x:ℝ . ⊦ (d- M E) ≐ x
         ❘ meta ?MetaAnnotations?label "dME"
         ❘ meta ?MetaAnnotations?description "The distance from point M to point E, effectively being the Radius."
        ❙

        dMT: Σ x:ℝ . ⊦ (d- M T) ≐ x
         ❘ meta ?MetaAnnotations?label "dBC"
         ❘ meta ?MetaAnnotations?description "The distance from point M to point T, the height of the cylinder."
        ❙

        rEMT: ⊦ (∠ E,M,T) ≐ 90.0
         ❘ meta ?MetaAnnotations?label "rEMT"
         ❘ meta ?MetaAnnotations?description "A right angle between E, M and T, starting at E."
        ❙


        
    ❚
    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 T )
                ❘ meta ?MetaAnnotations?label s"Cylinder"
                ❘ meta ?MetaAnnotations?description s"The constructed Cylinder."
        ❙
    ❚
❚