Added CuboidType

source/DefaultSituationSpace.mmt

@@ -28,6 +28,7 @@ theory DefaultSituationSpace =
         include ?ConeVolumeScroll ❙
         include ?TruncatedConeVolumeScroll ❙
         include ?RectangleScroll ❙
+        include ?CuboidScroll ❙
         
 
 

source/MetaTheories.mmt

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

source/Scrolls/CuboidScroll.mmt

+
+/T Miscellaneous scrolls for playing around/testing that don't have a good home yet  ❚
+
+/T Miscellaneous scrolls for playing around/testing that don't have a good home yet  ❚
+namespace http://mathhub.info/FrameIT/frameworld ❚
+fixmeta ?FrameworldMeta ❚
+
+
+theory CuboidScroll =
+    meta ?MetaAnnotations?problemTheory  ?CuboidScroll/Problem ❙
+    meta ?MetaAnnotations?solutionTheory ?CuboidScroll/Solution ❙
+    theory Problem =
+        R: Rectangle
+         ❘ meta ?MetaAnnotations?label "R"
+         ❘ meta ?MetaAnnotations?description "The given rectangle"
+        ❙
+        T: point
+         ❘ meta ?MetaAnnotations?label "T"
+         ❘ meta ?MetaAnnotations?description "The point above the centerpoint of the rectangle"
+        ❙
+
+        rTBA: ⊦ (∠ T,(R _getB),(R _getA)) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label "rTBA"
+         ❘ meta ?MetaAnnotations?description "A right angle between TBA, where B is the point enclosed by T and A"
+        ❙
+
+        rTBC: ⊦ (∠ T,(R _getB),(R _getC)) ≐ 90.0
+         ❘ meta ?MetaAnnotations?label "rTBC"
+         ❘ meta ?MetaAnnotations?description "A right angle between TBC, where B is the point enclosed by T and C"
+        ❙
+
+
+
+
+    ❙
+        
+    ❚
+    theory Solution =
+        include ?CuboidScroll/Problem ❙
+        meta ?MetaAnnotations?label "Cuboid" ❙
+        meta ?MetaAnnotations?description s"Given a rectangle and a top point that lies above the point in the center of the right-angle formed by the squarepoints
+                                            this scroll constructs a cuboid. Additionally you need a proof that there are two right angles between TBC and TBA" ❙
+        ConstructedCuboid : Cuboid
+                ❘ = CuboidCons R T
+                ❘ meta ?MetaAnnotations?label s"Cuboid"
+                ❘ meta ?MetaAnnotations?description s"The constructed Cuboid."
+        ❙
+    ❚
+❚
\ No newline at end of file

source/Scrolls/CuboidType.mmt

+namespace http://mathhub.info/FrameIT/frameworld ❚
+fixmeta ur:?LF ❚
+
+theory CuboidType =
+  
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ?FrameITBasics ❙
+
+  cuboidType : type ❘ # Cuboid ❙
+  cuboidCons : Rectangle ⟶ point  ⟶ Cuboid  ❘ # CuboidCons 1 2 ❙
+  
+❚
\ No newline at end of file

source/Scrolls/RectangleScroll.mmt

@@ -23,7 +23,7 @@ theory RectangleScroll =
          ❘ meta ?MetaAnnotations?description "The third point"
         ❙
 
-        rC: ⊦ (∠ A,B,C) ≐ 90.0
+        rABC: ⊦ (∠ A,B,C) ≐ 90.0
          ❘ meta ?MetaAnnotations?label "rC"
          ❘ meta ?MetaAnnotations?description "A right angle between ABC, where B is the point enclosed by A and B"
         ❙

source/Scrolls/RectangleType.mmt

@@ -9,4 +9,11 @@ theory RectangleType =
   rectangleType : type ❘ # Rectangle ❙
   rectangleCons : point ⟶ point ⟶ point  ⟶ Rectangle  ❘ # RectangleCons 1 2 3 ❙
   
+  getA : Rectangle ⟶ point ❘ # 1 _getA ❙
+  getB : Rectangle ⟶ point ❘ # 1 _getB ❙
+  getC : Rectangle ⟶ point ❘ # 1 _getC ❙
+
+  axiomgetA : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ A ❙
+  axiomgetB : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ B ❙
+  axiomgetC : {R: Rectangle} ⊦ (RectangleCons A B C) ≐ C ❙
 ❚
\ No newline at end of file