Commit dfa210b2 authored by bBoesl's avatar bBoesl

23.10

parent 0d19de60
......@@ -16,7 +16,7 @@ theory standartMathStuff : http://mathhub.info/MitM/Foundation?Math =
theory Vector : http://mathhub.info/MitM/Foundation?Math =
include ☞arith:?RealArithmetics ❙
include ?standartMathStuff ❙
include ☞algebra:?RealVectorspace ❙
// include ☞algebra:?RealVectorspace ❙
vector: type ❘ # V ❙
// vector: type ❘ = realVec3.universe❘ # V ❙ // works but is slow as sloth ❙
......
......@@ -21,31 +21,43 @@ theory ProblemTheory : http://BenniDoes.Stuff/?BenniDoesStuff =
E: V ❙
F: V ❙
distance_E_D_value : ℝ ❙
distance_E_D: ⊦ ( d E D) ≐ distance_E_D_value ❙
distance_E_B_value : ℝ ❙
distance_E_B: ⊦ ( d E B) ≐ distance_E_B_value ❙
distance_A_B_value : ℝ ❙
distance_A_B: ⊦ ( d A B) ≐ distance_A_B_value ❙
distance_A_D_value : ℝ ❙
distance_A_D: ⊦ ( d A D) ≐ distance_A_D_value ❙
distance_A_D_value : ℝ ❙
distance_A_D: ⊦ ( d A D) ≐ distance_A_D_value ❙
distance_B_C_value : ℝ ❙
distance_B_C: ⊦ ( d B C) ≐ distance_B_C_value ❙
distance_B_E_value : ℝ ❙
distance_B_E: ⊦ ( d B E) ≐ distance_B_E_value ❙
distance_C_E_value : ℝ ❙
distance_C_E: ⊦ ( d C E) ≐ distance_C_E_value ❙
distance_C_F_value : ℝ ❙
distance_C_F: ⊦ ( d C F) ≐ distance_C_F_value ❙
distance_D_F: ℝ ❙
distance_D_F: ⊦ (d D F) ≐ distance_D_F_value ❙
distance_E_D_value : ℝ ❙
distance_E_D: ⊦ ( d E D) ≐ distance_E_D_value ❙
distance_E_B_value : ℝ ❙
distance_E_B: ⊦ ( d E B) ≐ distance_E_B_value ❙
distance_E_F_value : ℝ ❙
distance_E_F: ⊦ ( d E F) ≐ distance_E_F_value ❙
distance_E_C_value : ℝ ❙
distance_E_F: ⊦ ( d E C) ≐ distance_E_C_value ❙
RightAngleProof: ⊦ ✓ ( ≺ B A D ) ❙
SamelengthProof_1: ⊦ distance A_D_value ≐ distance_A_B_value ❙
SamelengthProof_2: ⊦ distance E_D_value ≐ distance_E_B_value ❙
SamelengthProof_3: ⊦ distance E_D_value ≐ distance_A_B_value ❙
SamelengthProof_4: ⊦ distance A_D_value ≐ distance_E_B_value ❙
SumProof_1: ⊦ distance_C_F_value ≐ ( distance_C_E_value + distance_E_F_value )❙
SamelengthProof_1: ⊦ distance_A_D_value ≐ distance_E_B_value ❙
SamelengthProof_2: ⊦ distance_E_D_value ≐ distance_A_B_value ❙
......@@ -2,8 +2,6 @@ namespace http://BenniDoes.Stuff/ ❚
import mitm http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/smglom/arithmetics ❚
theory Planes : http://mathhub.info/MitM/Foundation?Math =
include ?Lines ❙
include ?Triangle ❙
......
namespace http://BenniDoes.Stuff/ ❚
// C ❚
// |\ ❚
// ~|~\~~~~~ ❚
// ~|~~\~~~~ ❚
// ~|~~~\~~~ ❚
// ~|~~~~\~~ ❚
// B|_____\E ❚
// | \ ❚
// | \ ❚
// |________\ ❚
// A F ❚
theory problemTheory : http://BenniDoes.Stuff/?BenniDoesStuff =
av : V ❙
bv : V ❙
cv : V ❙
ev : V ❙
fv : V ❙
distance_a_b_value : ℝ ❙
distance_a_b: ⊦ ( d av bv ) ≐ distance_a_b_value ❙
distance_a_f_value: ℝ ❙
distance_a_f: ⊦ ( d av fv ) ≐ ( distance_a_f_value ) ❙
distance_b_e_value : ℝ ❙
distance_b_e: ⊦ ( d bv ev ) ≐ distance_b_e_value ❙
buildLineProof_a_b_c: ⊦ ( ∖ av bv cv) ❙
buildLineProof_c_e_f: ⊦ ( ∖ cv ev fv) ❙
proofLinesnotSame: ⊦ ¬ ( (av ⁻ cv) ∥ (cv ⁻ fv) ) ❙
parallelHeightsProof: ⊦ (av ⁻ fv) ∥ (bv ⁻ ev) ❙
theory situationTherory : http://BenniDoes.Stuff/?BenniDoesStuff =
sa: V ❙
sb: V ❙
sc: V ❙
se: V ❙
sf: V ❙
sdistance_a_b_value = 5.0 ❙
sdistance_a_b: ⊦ ( d sa sb ) ≐ sdistance_a_b_value ❙
sdistance_a_f_value = 5.0 ❙
sdistance_a_f: ⊦ ( d sa sf ) ≐ sdistance_a_f_value ❙
sdistance_b_e_value = 1.0 ❙
sdistance_b_e: ⊦ ( d sb se ) ≐ sdistance_b_e_value ❙
sbuildLineProof_a_b_c: ⊦ ( ∖ sa sb sc) ❙
sbuildLineProof_c_e_f: ⊦ ( ∖ sc se sf) ❙
sproofLinesnotSame: ⊦ ¬ ( (sa ⁻ sc) ∥ (sc ⁻ sf) ) ❙
sparallelHeightsProof: ⊦ (sa ⁻ sf) ∥ (sb ⁻ se) ❙
theory solutionTherory : http://BenniDoes.Stuff/?BenniDoesStuff =
include ?problemTheory ❙
distance_a_c_value : ℝ ❘ = distance_a_b_value ⋅ distance_a_f_value / distance_b_e_value ❙
distance_a_c: ⊦ ( d av cv ) ≐ distance_a_c_value ❙
view situationProblemView : ?problemTheory -> ?situationTherory =
av = sa ❙
bv = sb ❙
cv = sc ❙
ev = se ❙
fv = sf ❙
distance_a_b_value = sdistance_a_b_value ❙
distance_a_b = sdistance_a_b ❙
distance_a_f_value = sdistance_a_f_value ❙
distance_a_f = sdistance_a_f ❙
distance_b_e_value = sdistance_b_e_value ❙
distance_b_e = sdistance_b_e ❙
buildLineProof_a_b_c = sbuildLineProof_a_b_c ❙
buildLineProof_c_e_f = sbuildLineProof_c_e_f ❙
proofLinesnotSame = sproofLinesnotSame ❙
parallelHeightsProof = sparallelHeightsProof ❙
\ No newline at end of file
namespace http://BenniDoes.Stuff/ ❚
//
A
|\~~~~~~~~
|~\~~~~~~
|__\___F
B C\ |
\ |
\|
E
theory problemTheory : http://BenniDoes.Stuff/?BenniDoesStuff =
av : V ❙
bv : V ❙
cv : V ❙
ev : V ❙
fv : V ❙
distance_b_c_value : ℝ ❙
distance_b_c: ⊦ ( d bv cv ) ≐ distance_b_c_value ❙
distance_c_f_value: ℝ ❙
distance_c_f: ⊦ ( d cv fv ) ≐ ( distance_c_f_value ) ❙
distance_e_f_value : ℝ ❙
distance_e_f: ⊦ ( d ev fv ) ≐ distance_e_f_value ❙
buildLineProof_a_c_e: ⊦ ( ∖ av cv ev) ❙
buildLineProof_b_c_f: ⊦ ( ∖ bv cv fv) ❙
proofLinesnotSame: ⊦ ¬ ( (av ⁻ ev) ∥ (bv ⁻ fv) ) ❙
parallelHeightsProof: ⊦ (av ⁻ bv) ∥ (ev ⁻ fv) ❙
theory situationTherory : http://BenniDoes.Stuff/?BenniDoesStuff =
sa: V ❙
sb: V ❙
sc: V ❙
se: V ❙
sf: V ❙
sdistance_b_c_value = 5.0 ❙
sdistance_b_c: ⊦ ( d sb sc ) ≐ sdistance_b_c_value ❙
sdistance_c_f_value = 5.0 ❙
sdistance_c_f: ⊦ ( d sc sf ) ≐ sdistance_c_f_value ❙
sdistance_e_f_value = 1.0 ❙
sdistance_e_f: ⊦ ( d se sf ) ≐ sdistance_e_f_value ❙
sbuildLineProof_a_c_e: ⊦ ( ∖ sa sc se) ❙
sbuildLineProof_b_c_f: ⊦ ( ∖ sb sc sf) ❙
sproofLinesnotSame: ⊦ ¬ ( (sa ⁻ se) ∥ (sb ⁻ sf) ) ❙
sparallelHeightsProof: ⊦ (sa ⁻ sb) ∥ (se ⁻ sf) ❙
theory solutionTherory : http://BenniDoes.Stuff/?BenniDoesStuff =
include ?problemTheory ❙
distance_a_b_value : ℝ ❘ = distance_a_c_value ⋅ distance_e_f_value / distance_c_f_value ❙
distance_a_b: ⊦ ( d av bv ) ≐ distance_a_b_value ❙
view situationProblemView : ?problemTheory -> ?situationTherory =
av = sa ❙
bv = sb ❙
cv = sc ❙
ev = se ❙
fv = sf ❙
distance_a_b_value = sdistance_a_b_value ❙
distance_a_b = sdistance_a_b ❙
distance_a_f_value = sdistance_a_f_value ❙
distance_a_f = sdistance_a_f ❙
distance_b_e_value = sdistance_b_e_value ❙
distance_b_e = sdistance_b_e ❙
buildLineProof_a_c_e = sbuildLineProof_a_c_e ❙
buildLineProof_c_e_f = sbuildLineProof_c_e_f ❙
proofLinesnotSame = sproofLinesnotSame ❙
parallelHeightsProof = sparallelHeightsProof ❙
\ No newline at end of file
......@@ -14,29 +14,29 @@ namespace http://BenniDoes.Stuff/ ❚
theory problemTheory : http://BenniDoes.Stuff/?BenniDoesStuff =
a : V ❙
b : V ❙
c : V ❙
e : V ❙
f : V ❙
av : V ❙
bv : V ❙
cv : V ❙
ev : V ❙
fv : V ❙
distance_a_b_value : ℝ ❙
distance_a_b: ⊦ ( d a b ) ≐ distance_a_b_value ❙
distance_a_b: ⊦ ( d av bv ) ≐ distance_a_b_value ❙
distance_b_c_value : ℝ ❙
distance_b_c: ⊦ ( d b c ) ≐ distance_b_c_value ❙
distance_b_c: ⊦ ( d bv cv ) ≐ distance_b_c_value ❙
distance_a_c: ⊦ ( d a c ) ≐ ( distance_a_b_value + distance_b_c_value ) ❙
distance_a_c: ⊦ ( d av cv ) ≐ ( distance_a_b_value + distance_b_c_value ) ❙
distance_b_e_value : ℝ ❙
distance_b_e: ⊦ ( d b e ) ≐ distance_b_e_value ❙
distance_b_e: ⊦ ( d bv ev) ≐ distance_b_e_value ❙
buildLineProof_a_b_c: ⊦ ( ∖ a b c) ❙
buildLineProof_c_e_f: ⊦ ( ∖ c e f) ❙
proofLinesnotSame: ⊦ ¬ ( (a ⁻ c) ∥ (c ⁻ f) ) ❙
buildLineProof_a_b_c: ⊦ ( ∖ av bv cv) ❙
buildLineProof_c_e_f: ⊦ ( ∖ cv ev fv) ❙
proofLinesnotSame: ⊦ ¬ ( (av ⁻ cv) ∥ (cv ⁻ fv) ) ❙
parallelHeightsProof: ⊦ (a ⁻ f) ∥ (b ⁻ e) ❙
parallelHeightsProof: ⊦ (av ⁻ fv) ∥ (bv ⁻ ev) ❙
theory situationTherory : http://BenniDoes.Stuff/?BenniDoesStuff =
......@@ -71,17 +71,17 @@ theory situationTherory : http://BenniDoes.Stuff/?BenniDoesStuff =
theory solutionTherory : http://BenniDoes.Stuff/?BenniDoesStuff =
include ?problemTheory ❙
distance_a_f_value : ℝ ❘ = distance_b_e_value ⋅ ( d a c ) / distance_a_b_value ❙
distance_a_f: ⊦ ( d a f ) ≐ distance_a_f_value ❙
distance_a_f_value : ℝ ❘ = distance_b_e_value ⋅ ( d av cv ) / distance_a_b_value ❙
distance_a_f: ⊦ ( d av fv ) ≐ distance_a_f_value ❙
view situationProblemView : ?problemTheory -> ?situationTherory =
a = sa ❙
b = sb ❙
c = sc ❙
e = se ❙
f = sf ❙
av = sa ❙
bv = sb ❙
cv = sc ❙
ev = se ❙
fv = sf ❙
distance_a_b_value = sdistance_b_c_value ❙
distance_a_b = sdistance_a_b ❙
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment