Commit 9f6b0dc9 by Benjamin Bösl

### began smglomming of my stuff, its slow

parent 20bbf96c
This diff is collapsed.
mmtrc deleted 100644 → 0
 #backends lmh . \ No newline at end of file
 \ No newline at end of file
 namespace http://BenniDoes.Stuff/ ❚ import mitm http://mathhub.info/MitM/Foundation ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ import algebra http://mathhub.info/MitM/smglom/algebra ❚ theory standartMathStuff : http://mathhub.info/MitM/Foundation?Math = include arith:?RealArithmetics ❙ include ☞arith:?RealArithmetics ❙ Pi : ℝ ❘ # π ❙ cos: ℝ ⟶ ℝ ❘ # cos 1❙ arccos: ℝ ⟶ ℝ ❘ # arccos 1❙ ... ... @@ -12,18 +13,21 @@ theory standartMathStuff : http://mathhub.info/MitM/Foundation?Math = theory 3DVector : http://mathhub.info/MitM/Foundation?Math = include arith:?RealArithmetics ❙ theory Vector : http://mathhub.info/MitM/Foundation?Math = include ☞arith:?RealArithmetics ❙ include ?standartMathStuff ❙ include ☞algebra:?RealVectorspace ❙ vector: type ❘ # V ❙ vector: type ❘ # V ❙ // 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 ❙ v_2: V ⟶ ℝ ❘ # _y 1 prec 50 ❙ v_3: V ⟶ ℝ ❘ # _z 1 prec 50 ❙ vec_add: V ⟶ V ⟶ V ❘ = [v, w] Vof ( ( _x v ) + ( _x w ) ) ( ( _y v ) + ( _y w ) ) ( ( _z v ) + ( _z w ) ) ❘ # 1 ⁺ 2 ❙ // jsuperplus ❙ vec_add: V ⟶ V ⟶ V ❘ = [v, w] Vof ( ( _x v ) + ( _x w ) ) ( ( _y v ) + ( _y w ) ) ( ( _z v ) + ( _z w ) ) ❘ # 1 ⁺ 2 ❙ // jsuperplus ❙ // vec_add = realVec3.op ❘ # 1 ⁺ 2 ❙ vec_sub: V ⟶ V ⟶ V ❘ = [v, w] Vof ( ( _x v ) - ( _x w ) ) ( ( _y v ) - ( _y w ) ) ( ( _z v ) - ( _z w ) ) ❘ # 1 ⁻ 2 ❙ // jsuperminus ❙ vec_mult: ℝ ⟶ V ⟶ V ❘ # 1 ** 2❙ scalarproduct: V ⟶ V ⟶ ℝ ❘ = [v,w] ( _x v) ⋅ ( _x w) + ( _y v) ⋅ ( _y w) + ( _z v) ⋅ ( _z w) ❘ # < 1 , 2 > ❙ ... ...
 namespace http://BenniDoes.Stuff/ ❚ theory BenniDoesStuff : http://mathhub.info/MitM/Foundation?Math = include http://BenniDoes.Stuff/?3DVector ❙ include http://BenniDoes.Stuff/?Lines ❙ include http://BenniDoes.Stuff/?InterceptTheorem ❙ include http://BenniDoes.Stuff/?Triangle ❙ include http://BenniDoes.Stuff/?Pythagoras ❙ include http://BenniDoes.Stuff/?Planes ❙ include ☞http://BenniDoes.Stuff/?Vector ❙ include ☞http://BenniDoes.Stuff/?Lines ❙ include ☞http://BenniDoes.Stuff/?InterceptTheorem ❙ include ☞http://BenniDoes.Stuff/?Triangle ❙ include ☞http://BenniDoes.Stuff/?Pythagoras ❙ include ☞http://BenniDoes.Stuff/?Planes ❙ ❚ \ No newline at end of file
 ... ... @@ -3,7 +3,7 @@ import mitm http://mathhub.info/MitM/Foundation ❚ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory Lines : http://mathhub.info/MitM/Foundation?Math = include ?3DVector ❙ include ?Vector ❙ include ?Planes ❙ // point: V ❙ ... ...
 ... ... @@ -6,7 +6,7 @@ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory Triangle : http://mathhub.info/MitM/Foundation?Math = include ?3DVector ❙ include ?Vector ❙ include ?Lines ❙ triangle: type ❘ # Δ ❙ ... ... @@ -56,38 +56,38 @@ theory Triangle : http://mathhub.info/MitM/Foundation?Math = theory Pythagoras : http://mathhub.info/MitM/Foundation?Math = include ?Triangle ❙ pythagoras_α = [T] ⊦ ( _c T) ⋅ ( _c T) + ( _b T) ⋅ ( _b T) ≐ ( _a T) ⋅ ( _a T) ❙ pythagoras_β = [T] ⊦ ( _a T) ⋅ ( _a T) + ( _c T) ⋅ ( _c T) ≐ ( _b T) ⋅ ( _b T) ❙ pythagoras_γ = [T] ⊦ ( _a T) ⋅ ( _a T) + ( _b T) ⋅ ( _b T) ≐ ( _c T) ⋅ ( _c T) ❙ pythagoras_α = [T] ( _c T) ⋅ ( _c T) + ( _b T) ⋅ ( _b T) ≐ ( _a T) ⋅ ( _a T) ❙ pythagoras_β = [T] ( _a T) ⋅ ( _a T) + ( _c T) ⋅ ( _c T) ≐ ( _b T) ⋅ ( _b T) ❙ pythagoras_γ = [T] ( _a T) ⋅ ( _a T) + ( _b T) ⋅ ( _b T) ≐ ( _c T) ⋅ ( _c T) ❙ pythagoras_theorem : {T} { p : ⊦ ( ✓ _α T ) } pythagoras_α T ❙ pythagoras_theorem : {T} { p : ⊦ ( ✓ _β T ) } pythagoras_β T ❙ pythagoras_theorem : {T} { p : ⊦ ( ✓ _γ T ) } pythagoras_γ T ❙ pythagoras_theorem_α : {T} { p : ⊦ ( ✓ _α T ) } ⊦ pythagoras_α T ❙ pythagoras_theorem_β : {T} { p : ⊦ ( ✓ _β T ) } ⊦ pythagoras_β T ❙ pythagoras_theorem_γ : {T} { p : ⊦ ( ✓ _γ T ) } ⊦ pythagoras_γ T ❙ geometric_mean_α = [T] ⊦ ( _ha T ⋅ _ha T ) ≐ ( d ( _haV T ) ( _B T ) ) ⋅ ( d ( _haV T) ( _C T ) ) ❙ geometric_mean_β = [T] ⊦ ( _hb T ⋅ _hb T ) ≐ ( d ( _hbV T ) ( _A T ) ) ⋅ ( d ( _hbV T) ( _C T ) ) ❙ geometric_mean_γ = [T] ⊦ ( _hc T ⋅ _hc T ) ≐ ( d ( _hcV T ) ( _B T ) ) ⋅ ( d ( _hcV T) ( _A T ) ) ❙ geometric_mean_α = [T] ( _ha T ⋅ _ha T ) ≐ ( d ( _haV T ) ( _B T ) ) ⋅ ( d ( _haV T) ( _C T ) ) ❙ geometric_mean_β = [T] ( _hb T ⋅ _hb T ) ≐ ( d ( _hbV T ) ( _A T ) ) ⋅ ( d ( _hbV T) ( _C T ) ) ❙ geometric_mean_γ = [T] ( _hc T ⋅ _hc T ) ≐ ( d ( _hcV T ) ( _B T ) ) ⋅ ( d ( _hcV T) ( _A T ) ) ❙ geometric_mean_theorem : {T} { p : ⊦ ( ✓ _α T ) } geometric_mean_α T ❙ geometric_mean_theorem : {T} { p : ⊦ ( ✓ _β T ) } geometric_mean_β T ❙ geometric_mean_theorem : {T} { p : ⊦ ( ✓ _γ T ) } geometric_mean_γ T ❙ geometric_mean_theorem_α : {T} { p : ⊦ ( ✓ _α T ) } ⊦ geometric_mean_α T ❙ geometric_mean_theorem_β : {T} { p : ⊦ ( ✓ _β T ) } ⊦ geometric_mean_β T ❙ geometric_mean_theorem_γ : {T} { p : ⊦ ( ✓ _γ T ) } ⊦ geometric_mean_γ T ❙ cathetus_α_1 = [T] ⊦ ( _b T ⋅ _b T ) ≐ _a T ⋅ ( d ( _haV T) ( _C T ) )❙ cathetus_α_2 = [T] ⊦ ( _c T ⋅ _c T ) ≐ _a T ⋅ ( d ( _haV T) ( _B T ) )❙ cathetus_α_1 = [T] ( _b T ⋅ _b T ) ≐ _a T ⋅ ( d ( _haV T) ( _C T ) )❙ cathetus_α_2 = [T] ( _c T ⋅ _c T ) ≐ _a T ⋅ ( d ( _haV T) ( _B T ) )❙ cathetus_β_1 = [T] ⊦ ( _c T ⋅ _c T ) ≐ _b T ⋅ ( d ( _hbV T) ( _A T ) )❙ cathetus_β_2 = [T] ⊦ ( _a T ⋅ _a T ) ≐ _b T ⋅ ( d ( _hbV T) ( _C T ) )❙ cathetus_β_1 = [T] ( _c T ⋅ _c T ) ≐ _b T ⋅ ( d ( _hbV T) ( _A T ) )❙ cathetus_β_2 = [T] ( _a T ⋅ _a T ) ≐ _b T ⋅ ( d ( _hbV T) ( _C T ) )❙ cathetus_γ_1 = [T] ⊦ ( _a T ⋅ _a T ) ≐ _c T ⋅ ( d ( _hcV T) ( _B T ) )❙ cathetus_γ_2 = [T] ⊦ ( _b T ⋅ _b T ) ≐ _c T ⋅ ( d ( _hcV T) ( _A T ) )❙ cathetus_γ_1 = [T] ( _a T ⋅ _a T ) ≐ _c T ⋅ ( d ( _hcV T) ( _B T ) )❙ cathetus_γ_2 = [T] ( _b T ⋅ _b T ) ≐ _c T ⋅ ( d ( _hcV T) ( _A T ) )❙ catheus_theorem : {T} { p : ⊦ ( ✓ _α T ) } cathetus_α_1 T ❙ catheus_theorem : {T} { p : ⊦ ( ✓ _α T ) } cathetus_α_2 T ❙ catheus_theorem_α_1 : {T} { p : ⊦ ( ✓ _α T ) } ⊦ cathetus_α_1 T ❙ catheus_theorem_α_2 : {T} { p : ⊦ ( ✓ _α T ) } ⊦ cathetus_α_2 T ❙ catheus_theorem : {T} { p : ⊦ ( ✓ _β T ) } cathetus_β_1 T ❙ catheus_theorem : {T} { p : ⊦ ( ✓ _β T ) } cathetus_β_2 T ❙ catheus_theorem_β_1 : {T} { p : ⊦ ( ✓ _β T ) } ⊦ cathetus_β_1 T ❙ catheus_theorem_β_2 : {T} { p : ⊦ ( ✓ _β T ) } ⊦ cathetus_β_2 T ❙ catheus_theorem : {T} { p : ⊦ ( ✓ _γ T ) } cathetus_γ_1 T ❙ catheus_theorem : {T} { p : ⊦ ( ✓ _γ T ) } cathetus_γ_2 T ❙ catheus_theorem_γ_1 : {T} { p : ⊦ ( ✓ _γ T ) } ⊦ cathetus_γ_1 T ❙ catheus_theorem_γ_2 : {T} { p : ⊦ ( ✓ _γ T ) } ⊦ cathetus_γ_2 T ❙ ❚ \ No newline at end of file
 extension info.kwarc.mmt.odk.Plugin \ 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!