PrismScroll.mmt

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

theory PrismScroll =
    meta ?MetaAnnotations?problemTheory  ?PrismScroll/Problem ❙
    meta ?MetaAnnotations?solutionTheory ?PrismScroll/Solution ❙

    theory Problem =
        T: triangle
            ❘ meta ?MetaAnnotations?label "T"
            ❘ meta ?MetaAnnotations?description "Triangle"
        ❙
        D: point
            ❘ meta ?MetaAnnotations?label "D"
            ❘ meta ?MetaAnnotations?description "Point D"
        ❙
        dAB: Σ x:ℝ . ⊦ (d- (triangle_point1 T) D) ≐ x
         ❘ meta ?MetaAnnotations?label s"d${lverb (triangle_point1 T) D}"
         ❘ meta ?MetaAnnotations?description s"The distance from point ${lverb (triangle_point1 T)} to point ${lverb D}"
        ❙
        rDAB: ⊦ (angle_between D (triangle_point1 T) (triangle_point2 T)) ≐ 90.0
         ❘ meta ?MetaAnnotations?label s"r${lverb D}"
         ❘ meta ?MetaAnnotations?description s"A right angle between ${lverb D,(triangle_point1 T),(triangle_point2 T)}, where ${lverb D} is the point enclosed by ${lverb (triangle_point1 T)} and ${lverb (triangle_point1 T)}"
        ❙
        rDAC: ⊦ (angle_between D (triangle_point1 T) (triangle_point3 T)) ≐ 90.0
         ❘ meta ?MetaAnnotations?label s"r${lverb D}"
         ❘ meta ?MetaAnnotations?description s"A right angle between ${lverb D,(triangle_point1 T),(triangle_point3 T)}, where ${lverb D} is the point enclosed by ${lverb (triangle_point1 T)} and ${lverb (triangle_point3 T)}"
        ❙
    ❚

    theory Solution =
        include ?PrismScroll/Problem ❙

        meta ?MetaAnnotations?label "Prism" ❙
        meta ?MetaAnnotations?description "Scrolls that takes three points and constructs a Prism." ❙

        ConstructedPrism : Prism
                ❘ = (PrismCons T D)
                ❘ meta ?MetaAnnotations?label "Prism"
                ❘ meta ?MetaAnnotations?description "The constructed Prism."
        ❙
    ❚
❚