Triangle added

source/DefaultSituationSpace.mmt

@@ -7,8 +7,8 @@ theory DefaultSituationSpace =
         include ?SupplementaryAngles ❙
         include ?OppositeLen ❙
         include ?AngleSum ❙
-      //  include ?ParallelLines ❙
-	 //   include ?InterceptTheorem ❙
+        // include ?ParallelLines ❙
+	    // include ?InterceptTheorem ❙
 	    include ?Pythagoras❙
 	    include ?CylinderVolumeScroll❙
 		include ?CircleLineAngleToAngleScroll❙
@@ -17,18 +17,18 @@ theory DefaultSituationSpace =
         include ?Test ❙
         include ?CircleScroll ❙
         
-        include ?MuchBetterCircleScroll ❙
 		include ?BouncingScroll ❙
         include ?WBouncingScroll ❙
         include ?W3DBouncingScroll ❙
         include ?T3DBouncingScroll ❙
-      //  include ?SinOppositeLeg ❙
+        // include ?SinOppositeLeg ❙
         include ?CircleLineAngleScroll ❙
         include ?CircleAreaScroll ❙
         include ?ConeVolumeScroll ❙
         include ?TruncatedConeVolumeScroll ❙
         include ?RectangleScroll ❙
         include ?CuboidScroll ❙
+        include ?TriangleScroll ❙
         
 
 

source/MetaTheories.mmt

@@ -337,6 +337,7 @@ theory FrameworldMeta =
   include ?FrameITTheories ❙
   include ?RectangleType ❙
   include ?CuboidType ❙
+  include ?TriangleType ❙
 
  // include ☞http://mathhub.info/MitM/core/arithmetics?RealArithmetics ❙
 

source/Scrolls/MuchBetterCircleScroll.mmt

-namespace http://mathhub.info/FrameIT/frameworld ❚
-fixmeta ?FrameworldMeta ❚
-
-/T This scrolls infers a 2D circle from three dedicated 3D points (the circle's supposed center,
-   one of the supposed circle itself, one in the plane the circle should lie in).
-❚
-theory MuchBetterCircleScroll =
-    meta ?MetaAnnotations?problemTheory ?MuchBetterCircleScroll/Problem ❙
-    meta ?MetaAnnotations?solutionTheory ?MuchBetterCircleScroll/Solution ❙
-
-    // the three special points M, A and  B ❙
-    theory Problem =
-        M : point ❘ meta ?MetaAnnotations?label "M"
-                  ❘ meta ?MetaAnnotations?description "The circle's center" ❙
-        A : point ❘ meta ?MetaAnnotations?label "A"
-                  ❘ meta ?MetaAnnotations?description "A point on the circle" ❙
-        B : point ❘ meta ?MetaAnnotations?label "B"
-                  ❘ meta ?MetaAnnotations?description "A point within the plane the circle should lie in." ❙
-        radiusC: Σ x:ℝ . ⊦ (d- M A ≐ x) ∨ (d- A M)
-               ❘ meta ?MetaAnnotations?label "r"
-               ❘ meta ?MetaAnnotations?description s"radius of the circle ${lverb cir}"
-        ❙
-    ❚
-
-    theory Solution =
-        include ?MuchBetterCircleScroll/Problem ❙
-
-        deduceC: circle
-              ❘ = ( pointsToC M A B )
-              ❘ meta ?MetaAnnotations?label s"○${lverb M}"
-              ❘ meta ?MetaAnnotations?description "Circle"
-        ❙
-
-        deduceR:  Σ x:ℝ . ⊦ ( circleRadius deduceC) ≐ x
-              ❘ =  ⟨ d- M A , sketch "deduce Radius"⟩
-              ❘ meta ?MetaAnnotations?label s"r${lverb deduceC}"
-              ❘ meta ?MetaAnnotations?description s"radius of ${lverb deduceC} (radius fact)"  b
-        ❙
-
-        deduceR2:  Σ x:ℝ . ⊦ ( d- A M ) ≐ x 
-                ❘ =  ⟨ d- A M , sketch "deduce Radius2"⟩
-                ❘ meta ?MetaAnnotations?label s"${lverb A M}"
-                ❘ meta ?MetaAnnotations?description s"radius of ${lverb deduceC} (distance fact)"
-        ❙
-
-        midOnCircle: ⊦ M VonC deduceC
-                   ❘ = midOnC deduceC M
-                   ❘ meta ?MetaAnnotations?label s"${lverb M}∈${lverb deduceC}"
-                   ❘ meta ?MetaAnnotations?description s"proof of M being on the circle ${lverb deduceC}"
-        ❙
-
-        edgeOnCircle: ⊦ A VonC deduceC
-                    ❘ meta ?MetaAnnotations?label s"${lverb A}∈${lverb deduceC}"
-                    ❘ meta ?MetaAnnotations?description s"proof of A being on the circle ${lverb deduceC}"
-        ❙
-
-        // the description verbalizes CircleCircumference, hence must come after its declaration ❙
-        meta ?MetaAnnotations?label "CircleScroll" ❙
-        meta ?MetaAnnotations?description s"Calculating a circle defined by the middle ${lverb M}, an edge point ${lverb A} and a point on the circle plane ${lverb B}. " ❙
-    ❚
-❚
\ No newline at end of file

source/Scrolls/TriangleScroll.mmt

+namespace http://mathhub.info/FrameIT/frameworld ❚
+fixmeta ?FrameworldMeta ❚
+
+theory TriangleScroll =
+    meta ?MetaAnnotations?problemTheory  ?TriangleScroll/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?TriangleScroll/Solution ❙
+
+    theory Problem =
+        A: point
+            ❘ meta ?MetaAnnotations?label "A"
+            ❘ meta ?MetaAnnotations?description "The first point"
+        ❙
+        B: point
+            ❘ meta ?MetaAnnotations?label "B"
+            ❘ meta ?MetaAnnotations?description "The second point"
+        ❙
+        C: point
+            ❘ meta ?MetaAnnotations?label "C"
+            ❘ meta ?MetaAnnotations?description "The third point"
+        ❙
+    ❚
+
+    theory Solution =
+        include ?TriangleScroll/Problem ❙
+
+        meta ?MetaAnnotations?label "Triangle" ❙
+        meta ?MetaAnnotations?description s"Scrolls that takes three points and constructs a triangle." ❙
+
+        ConstructedTriangle : Triangle
+                ❘ = TriangleCons A B C
+                ❘ meta ?MetaAnnotations?label s"Triangle"
+                ❘ meta ?MetaAnnotations?description s"The constructed Triangle."
+        ❙
+    ❚
+❚
\ No newline at end of file

source/Scrolls/TriangleType.mmt

+namespace http://mathhub.info/FrameIT/frameworld ❚
+fixmeta ur:?LF ❚
+
+theory TriangleType =
+    include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+    include ?FrameITBasics ❙
+
+    triangleType : type ❘ # Triangle ❙
+    triangleCons : point ⟶ point ⟶ point ⟶ Triangle ❘ # TriangleCons 1 2 3 ❙
+❚
\ No newline at end of file