Commit 251b2a8a by bBoesl

### framed simple triangle

parent dfa210b2
 ... ... @@ -4,7 +4,7 @@ import arith http://mathhub.info/MitM/smglom/arithmetics ❚ theory Lines : http://mathhub.info/MitM/Foundation?Math = include ?Vector ❙ include ?Planes ❙ // include ?Planes ❙ // point: V ❙ // direction: V ❙ ... ...
 ... ... @@ -14,4 +14,7 @@ theory Sphere : http://mathhub.info/MitM/Foundation?Math = inSphere: S ⟶ V ⟶ bool ❘ = [s, v] ( d ( Sm s ) ( v ) ) < ( Sr s ) ❘ # 2 VinS 1 ❙ 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 ❙ ❚ \ No newline at end of file
 ... ... @@ -26,6 +26,7 @@ theory problemTheory : http://BenniDoes.Stuff/?BenniDoesStuff = distance_b_c_value : ℝ ❙ distance_b_c: ⊦ ( d bv cv ) ≐ distance_b_c_value ❙ distance_a_c_value: ℝ ❙ distance_a_c: ⊦ ( d av cv ) ≐ ( distance_a_b_value + distance_b_c_value ) ❙ distance_b_e_value : ℝ ❙ ... ...
 namespace http://BenniDoes.Stuff/ ❚ theory problemTheory : http://BenniDoes.Stuff/?BenniDoesStuff = pA : V ❙ pB : V ❙ pC : V ❙ ❚ theory situationTherory : http://BenniDoes.Stuff/?BenniDoesStuff = sA: V ❘ = Vof 1 1 1❙ sB: V ❘ = Vof 0 0 0❙ sC: V ❘ = Vof 0 0 1❙ ❚ theory solutionTherory : http://BenniDoes.Stuff/?BenniDoesStuff = include ?problemTheory ❙ area : ℝ ❘ = AΔ ( Δof pA pB pC ) ❙ ❚ view situationProblemView : ?problemTheory -> ?situationTherory = pA = sA ❙ pB = sB ❙ pC = sC ❙ ❚ \ No newline at end of file
 ... ... @@ -49,7 +49,7 @@ theory Triangle : http://mathhub.info/MitM/Foundation?Math = lawOfSinesCB: { T } ⊦ _c T / sin ( _γ T ) ≐ _b T / sin ( _β T ) ❙ angleSum = {T} ⊦ (( _α T) + ( _β T) + ( _γ T) )≐ π ❙ area: Δ ⟶ ℝ ❘ = [T] ( _a T ) ⋅ ( _ha T ) ⋅ ( 1 / 2 )❘ # AΔ 1 ❙ area: Δ ⟶ ℝ ❘ = [T] ( n ( ( _A T ⁻ _B T ) Vcross ( _A T ⁻ _C T ) ) ) ⋅ ( 1 / 2 )❘ # AΔ 1 ❙ ❚ ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!