Commit 84e682ec by bBoesl

### pyramid

parent 251b2a8a
 ... ... @@ -19,7 +19,7 @@ theory Vector : http://mathhub.info/MitM/Foundation?Math = // include ☞algebra:?RealVectorspace ❙ vector: type ❘ # V ❙ // vector: type ❘ = realVec3.universe❘ # V ❙ // works but is slow as sloth ❙ // vector: type ❘ = realVec3.universe❘ # V ❙ // works but is slow as sloth ❙ vectorOf: ℝ ⟶ ℝ ⟶ ℝ ⟶ V ❘ # Vof 1 2 3 ❙ OV : V ❙ v_1: V ⟶ ℝ ❘ # _x 1 prec 50 ❙ ... ...
 namespace http://BenniDoes.Stuff/ ❚ import mitm http://mathhub.info/MitM/Foundation ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory Pyramid : http://mathhub.info/MitM/Foundation?Math = include ☞http://BenniDoes.Stuff/?Vector ❙ include ☞http://BenniDoes.Stuff/?Triangle ❙ Pyramid : type ❘ # Pyr ❙ pyramidOf : V ⟶ V ⟶ V ⟶ V ⟶ Pyr ❘ # Pyrof 1 2 3 4 ❙ P_A : Pyr ⟶ V ❘ # P_A 1❙ P_A_axiom : {a :V, b :V, c :V, dd :V } ⊦ ( P_A ( Pyrof a b c dd) ) ≐ a ❙ P_B : Pyr ⟶ V ❘ # P_B 1❙ P_B_axiom : {a :V, b :V, c :V, dd :V } ⊦ ( P_B ( Pyrof a b c dd) ) ≐ b ❙ P_C : Pyr ⟶ V ❘ # P_C 1❙ P_C_axiom : {a :V, b :V, c :V, dd :V } ⊦ ( P_C ( Pyrof a b c dd) ) ≐ c ❙ P_D : Pyr ⟶ V ❘ # P_D 1❙ P_D_axiom : {a :V, b :V, c :V, dd :V } ⊦ ( P_D ( Pyrof a b c dd) ) ≐ dd ❙ Volume_Pyramid: Pyr ⟶ ℝ ❘ = [p ] ( 1 / 6) ⋅ ( < ( ( ( P_B p ) ⁻ ( P_A p ) ) Vcross ( ( P_C p ) ⁻ ( P_A p ) ) ), (( P_D p ) ⁻ ( P_A p ) ) > ) ❘# VolofP 1 ❙ ❚ \ No newline at end of file
 ... ... @@ -15,6 +15,6 @@ theory Sphere : http://mathhub.info/MitM/Foundation?Math = collidesSphereLine: S ⟶ L ⟶ bool ❘ = [s,l] ∃ [v] ( v VonL l ) ∨ (v VinS s ) ❘ # 1 ScolL 2 ❙ circumfenceSphere: S ⟶ ℝ ❘ = [s] ( Sr s ) ⋅ 2 ⋅ π ❘ # CS 1 ❙ areaSphere : S ⟶ ℝ ❘ = [s] ( Sr s ) ⋅ ( Sr s ) ⋅ π ❘ # AS 1 ❙ circumfenceSphere: S ⟶ ℝ ❘ = [s] ( Sr s ) ⋅ ( Sr s) ⋅ 4 ⋅ π ❘ # CS 1 ❙ areaSphere : S ⟶ ℝ ❘ = [s] ( Sr s ) ⋅ ( Sr s ) ⋅ (Sr s) ⋅ ( 4 / 3 ) ⋅ π ❘ # AS 1 ❙ ❚ \ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!