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
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."
❙
❚
❚