Added Sphere

source/DefaultSituationSpace.mmt

@@ -14,7 +14,6 @@ theory DefaultSituationSpace =
 		include ?CircleLineAngleToAngleScroll❙
 
         include ?Midpoint ❙
-        include ?Test ❙
         include ?CircleScroll ❙
         
 		include ?BouncingScroll ❙
@@ -30,6 +29,7 @@ theory DefaultSituationSpace =
         include ?CuboidScroll ❙
         include ?TriangleScroll ❙
         include ?SimpleCircleScroll ❙
+        include ?SphereScroll ❙
         
 
 

source/MetaTheories.mmt

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

source/Scrolls/SphereScroll.mmt

 namespace http://mathhub.info/FrameIT/frameworld ❚
 fixmeta ?FrameworldMeta ❚
 
+theory SphereType =
+  
+  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
+  include ?FrameITBasics ❙
+
+  sphereType : type ❘ # Sphere ❙
+  sphereCons : point ⟶ point  ⟶ Sphere  ❘ # SphereCons 1 2 ❙
+  
+❚
+
 
 theory SphereScroll =
     meta ?MetaAnnotations?problemTheory  ?SphereScroll/Problem ❙
@@ -8,13 +18,18 @@ theory SphereScroll =
 
     theory Problem =
         
-        C: circle
-         ❘ meta ?MetaAnnotations?label "C"
-         ❘ meta ?MetaAnnotations?description "center-circle"
+        M: point
+         ❘ meta ?MetaAnnotations?label "M"
+         ❘ meta ?MetaAnnotations?description "Midpoint of the sphere"
         ❙
         T: point
          ❘ meta ?MetaAnnotations?label "T"
-         ❘ meta ?MetaAnnotations?description "The top point above the center circle. Has to be parallel to the normal or the normal"
+         ❘ meta ?MetaAnnotations?description "Point on the edge of the sphere"
+        ❙
+
+        dMT: Σ x:ℝ . ⊦ (d- M T) ≐ x
+         ❘ meta ?MetaAnnotations?label MT"
+         ❘ meta ?MetaAnnotations?description "The distance between the mid- and edgepoint (i.e. the radius)"
         ❙
 
 
@@ -23,12 +38,13 @@ theory SphereScroll =
         
     ❚
     theory Solution =
+
         include ?SphereScroll/Problem ❙
         meta ?MetaAnnotations?label "Sphere" ❙
-        meta ?MetaAnnotations?description s"Takes a circle and a point parallel to the normal, then constructs a Sphere." ❙
+        meta ?MetaAnnotations?description s"Takes a point as midpoint and an edgepoint, then constructs a Sphere." ❙
         
-        ConstructedRectangle : Rectangle
-                ❘ = ( SphereCons C T )
+        ConstructedSphere : Sphere
+                ❘ = ( SphereCons M T )
                 ❘ meta ?MetaAnnotations?label s"Sphere"
                 ❘ meta ?MetaAnnotations?description s"The constructed Sphere."
         ❙

source/Scrolls/SphereType.mmt

-namespace http://mathhub.info/FrameIT/frameworld ❚
-fixmeta ?FrameworldMeta ❚
-
-theory SphereType =
-  
-  include ☞http://mathhub.info/MitM/core/geometry?3DGeometry ❙
-  include ?FrameITBasics ❙
-
-  sphereType : type ❘ # Sphere ❙
-  sphereCons : circle ⟶ point  ⟶ Sphere  ❘ # SphereCons 1 2 ❙
-  
-❚
\ No newline at end of file