Skip to content
Snippets Groups Projects
Commit f0fb36e3 authored by Paul-Walcher's avatar Paul-Walcher
Browse files

added lengths and rightangle proof requirement for cylinder scroll

parent a4c8def6
No related branches found
No related tags found
No related merge requests found
......@@ -20,6 +20,21 @@ theory CylinderScroll =
❘ meta ?MetaAnnotations?description "The point directly above the point M"
dME: Σ x:ℝ . ⊦ (d- M E) ≐ x
❘ meta ?MetaAnnotations?label "dME"
❘ meta ?MetaAnnotations?description "The distance from point M to point E, effectively being the Radius."
dMT: Σ x:ℝ . ⊦ (d- M T) ≐ x
❘ meta ?MetaAnnotations?label "dBC"
❘ meta ?MetaAnnotations?description "The distance from point M to point T, the height of the cylinder."
rEMT: ⊦ (∠ E,M,T) ≐ 90.0
❘ meta ?MetaAnnotations?label "rEMT"
❘ meta ?MetaAnnotations?description "A right angle between E, M and T, starting at E."
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment