Newer
Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
/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."
❙
❚
❚