Commit d3ddc072 authored by bBoesl's avatar bBoesl

added spheres, added symm-Triangles

parent 9f6b0dc9
......@@ -7,5 +7,6 @@ theory BenniDoesStuff : http://mathhub.info/MitM/Foundation?Math =
include ☞http://BenniDoes.Stuff/?Triangle ❙
include ☞http://BenniDoes.Stuff/?Pythagoras ❙
include ☞http://BenniDoes.Stuff/?Planes ❙
include ☞http://BenniDoes.Stuff/?Sphere ❙
\ No newline at end of file
......@@ -13,13 +13,13 @@ theory Lines : http://mathhub.info/MitM/Foundation?Math =
lineDirection: L ⟶ V ❘ # Ldir 1 ❙
basepoint : L ⟶ V ❘ # Lbase 1 ❙
onLine : L ⟶ V ⟶ bool ❘ # 2 onL 1 ❙
buildLine : V ⟶ V ⟶ V ⟶ bool ❘ = [A,B,C] A onL ( Lof B C) ❘ # ∖ 1 2 3 ❙
sameLine: L ⟶ L ⟶ bool ❘ = [A ,B] ( Lbase( B ) onL A ) ∧ ( ( Ldir B ) ∥ ( Ldir A ) ) ❘ # Lsame 1 2❙
collideLine: L ⟶ L ⟶ bool ❘ = [A,B] ∃ [v] ( v onL A ) ∧ ( v onL B ) ❘ # colL 1 2 ❙
onLine : L ⟶ V ⟶ bool ❘ # 2 VonL 1 ❙
buildLine : V ⟶ V ⟶ V ⟶ bool ❘ = [A,B,C] A VonL ( Lof B C) ❘ # ∖ 1 2 3 ❙
sameLine: L ⟶ L ⟶ bool ❘ = [A ,B] ( Lbase( B ) VonL A ) ∧ ( ( Ldir B ) ∥ ( Ldir A ) ) ❘ # Lsame 1 2❙
collideLine: L ⟶ L ⟶ bool ❘ = [A,B] ∃ [v] ( v VonL A ) ∧ ( v VonL B ) ❘ # colL 1 2 ❙
// pointOfIntersection = [A :L , B: L , p1 : ⊦ colL A B, p2 : ⊦ ¬ sameL A B] OV ❙
pointOfIntersection : {A ,B } ( ⊦ colL A B ) ⟶ ( ⊦ ¬ Lsame A B ) ⟶ V ❘ # colLV 1 2 3 4 ❙
pointOfIntersectionAxiom: {A, B, p1, p2} ⊦ ( ( colLV A B p1 p2) onL A ) ∧ ( ( colLV A B p1 p2 ) onL B )❙
pointOfIntersectionAxiom: {A, B, p1, p2} ⊦ ( ( colLV A B p1 p2) VonL A ) ∧ ( ( colLV A B p1 p2 ) VonL B )❙
basepoint_axiom: {A, B} ⊦ Lbase ( Lof A B ) ≐ A ❙
// does it matter, if you ignore the opposite direction? ❙
......
......@@ -27,10 +27,10 @@ theory Planes : http://mathhub.info/MitM/Foundation?Math =
lineOnPlane : L ⟶ P ⟶ bool ❘= [l,p ] ( ( Lbase l ) VonP p ) ∧ ( ( Lbase l ) ⁺ ( Ldir l ) ) VonP p ❘# 1 LonP 2 ❙
LinePlaneCollisionPoint : { A, B } ( ⊦ Ldir A ⊥⊥ Pnormal B ) ⟶ V ❘ # colPLV 1 2 3 ❙
LinePlaneCollisionPointAxiom : {A , B, p1 } ⊦ ( colPLV A B p1 ) VonP B ∧ ( colPLV A B p1 ) onL A ❙
LinePlaneCollisionPointAxiom : {A , B, p1 } ⊦ ( colPLV A B p1 ) VonP B ∧ ( colPLV A B p1 ) VonL A ❙
parallelPlanes : P ⟶ P ⟶ bool ❘= [ p1 ,p2] ( Pnormal p1 ) ∥ ( Pnormal p2 ) ❘# 1 Ppar 2 prec 50 ❙
samePlae: P ⟶ P ⟶ bool ❘ = [ p1 , p2] ( Pbase p1 VonP p2 ) ∧ ( p1 Ppar p2 )❘# Psame 1 2❙
samePlane: P ⟶ P ⟶ bool ❘ = [ p1 , p2] ( Pbase p1 VonP p2 ) ∧ ( p1 Ppar p2 )❘# Psame 1 2❙
collidePlane : P ⟶ P ⟶ bool ❘ = [ A ,B ] ( ¬ A Ppar B ) ∨ Psame A B ❘ # colP 1 2 ❙
collisionLine: {A, B } ⊦ colP A B ⟶ ⊦ ¬ Psame A B ⟶ L ❘ # colPPL 1 2 3 4❙
......
namespace http://BenniDoes.Stuff/ ❚
theory Sphere : http://mathhub.info/MitM/Foundation?Math =
include ?Vector ❙
include ?Lines ❙
sphere: type ❘ # S ❙
sphereAround: V ⟶ ℝ ⟶ S ❘# So 1 2 ❙
center: S ⟶ V ❘ # Sm 1 ❙
centerAxiom: {m,r} ⊦ Sm ( So m r) ≐ m ❙
radius: S ⟶ ℝ ❘ # Sr 1 ❙
radiusAxiom : {m,r} ⊦ Sr (So m r) ≐ r ❙
onSphere: S ⟶ V ⟶ bool ❘ = [s, v] ( d ( Sm s ) ( v ) ) ≐ ( Sr s ) ❘ # 2 VonS 1 ❙
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 ❙
\ No newline at end of file
......@@ -29,15 +29,15 @@ theory Triangle : http://mathhub.info/MitM/Foundation?Math =
c_triangle: Δ ⟶ ℝ ❘ = [T] n( _A T ⁻ _B T) ❘ # _c 1 prec 50 ❙
ha_triangle_point: Δ ⟶ V ❘ # _haV 1 prec 50 ❙
ha_triangle_point_axiom: { T } ⊦ ( _haV T ) onL ( Lof ( _B T) ( _C T ) ) ∧ ( _haV T ⁻ _B T ) ⊥⊥ ( _haV T ⁻ _A T ) ❙
ha_triangle_point_axiom: { T } ⊦ ( _haV T ) VonL ( Lof ( _B T) ( _C T ) ) ∧ ( _haV T ⁻ _B T ) ⊥⊥ ( _haV T ⁻ _A T ) ❙
ha_triangle_lenght: Δ ⟶ ℝ ❘ = [T] d ( _A T ) ( _haV T )❘ # _ha 1 prec 50 ❙
hb_triangle_point: Δ ⟶ V ❘ # _hbV 1 prec 50 ❙
hb_triangle_point_axiom: { T } ⊦ ( _hbV T ) onL ( Lof ( _A T) ( _C T ) ) ∧ ( _hbV T ⁻ _A T ) ⊥⊥ ( _hbV T ⁻ _B T ) ❙
hb_triangle_point_axiom: { T } ⊦ ( _hbV T ) VonL ( Lof ( _A T) ( _C T ) ) ∧ ( _hbV T ⁻ _A T ) ⊥⊥ ( _hbV T ⁻ _B T ) ❙
hb_triangle_lenght: Δ ⟶ ℝ ❘ = [T] d ( _B T ) ( _hbV T )❘ # _hb 1 prec 50 ❙
hc_triangle_point: Δ ⟶ V ❘ # _hcV 1 prec 50❙
hc_triangle_point_axiom: { T } ⊦ ( _hcV T ) onL ( Lof ( _A T) ( _B T ) ) ∧ ( _hcV T ⁻ _A T ) ⊥⊥ ( _hbV T ⁻ _C T ) ❙
hc_triangle_point_axiom: { T } ⊦ ( _hcV T ) VonL ( Lof ( _A T) ( _B T ) ) ∧ ( _hcV T ⁻ _A T ) ⊥⊥ ( _hbV T ⁻ _C T ) ❙
hc_triangle_lenght: Δ ⟶ ℝ ❘ = [T] d ( _C T ) ( _hcV T )❘ # _hc 1 prec 50 ❙
lawOfCosineAlpha: { T } ⊦ ( _a T ⋅ _a T ) ≐ ( _b T ⋅ _b T ) + ( _c T ⋅ _c T ) + 2 ⋅ _b T ⋅ _c T ⋅ ( cos ( _α T ) )❙
......@@ -49,7 +49,24 @@ 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 )❘ # AT 1 ❙
area: Δ ⟶ ℝ ❘ = [T] ( _a T ) ⋅ ( _ha T ) ⋅ ( 1 / 2 )❘ # AΔ 1 ❙
theory SymmetricTriangles : http://mathhub.info/MitM/Foundation?Math =
include ?Triangle ❙
symmetric_α: Δ ⟶ bool ❘ = [T] _β T ≐ _γ T ❘ # sym_α 1 ❙
symmetric_β: Δ ⟶ bool ❘ = [T] _α T ≐ _γ T ❘ # sym_β 1 ❙
symmetric_γ: Δ ⟶ bool ❘ = [T] _α T ≐ _β T ❘ # sym_γ 1 ❙
symmetric_edges_α: {T} {p : ⊦ (sym_α T) } ⊦ _b T ≐ _c T ❙
symmetric_edges_β: {T} {p : ⊦ (sym_β T) } ⊦ _a T ≐ _c T ❙
symmetric_edges_γ: {T} {p : ⊦ (sym_γ T) } ⊦ _a T ≐ _b T ❙
symmetric_α_edges: {T} {p : ⊦ ( _b T ≐ _c T)} ⊦ sym_α T ❙
symmetric_β_edges: {T} {p : ⊦ ( _a T ≐ _c T)} ⊦ sym_β T ❙
symmetric_γ_edges: {T} {p : ⊦ ( _a T ≐ _b T)} ⊦ sym_γ T ❙
......
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