namespace http://mathhub.info/MitM/core/geometry ❚
import base http://mathhub.info/MitM/Foundation ❚
import arith http://mathhub.info/MitM/core/arithmetics ❚
// TODO: ❚
import rules scala://rules.core.mitm.mmt.kwarc.info ❚
fixmeta base:?Logic ❚
theory Geometry =
include ☞arith:?RealArithmetics ❙
include ☞base:?Trigonometry ❙
theory Common > point : type,
add : point ⟶ point ⟶ point,
subtract : point ⟶ point ⟶ point,
mult : ℝ ⟶ point ⟶ point,
scp : point ⟶ point ⟶ ℝ ❘ =
// ℝ^n ❙
point_add : point ⟶ point ⟶ point ❘ = add ❘ # 1 ++ 2 prec 12 ❙
point_subtract : point ⟶ point ⟶ point ❘ = subtract ❘ # 1 -- 2 prec 12 ❙
vec_mult : ℝ ⟶ point ⟶ point ❘ = mult ❘ # 1 ⋅⋅ 2 prec 22 ❙
scalar_product : point ⟶ point ⟶ ℝ ❘ = scp ❘ # < 1 , 2 > ❙
norm : point ⟶ ℝ ❘ = [p] √ <p,p> ❘ # | 1 | ❙
metric : point ⟶ point ⟶ ℝ ❘ = [p1,p2] | (p1 -- p2) | ❘ # d- 1 2 ❙
rule rules?MetricCommutative ❙
normalize: point ⟶ point ❘ = [v] (1 / ( | v | )) ⋅⋅ v ❘ # norm 1 ❙
// Angles ❙
angle: point ⟶ point ⟶ ℝ ❘ = [v,w] acos ( < v,w > / (|v| ⋅ |w|)) ❘ # ∠ 1 2 prec 1 ❙
angle_between: point ⟶ point ⟶ point ⟶ ℝ ❘ = [x,y,z] ∠ (x -- y) (z -- y) ❘ # ∠ 1 , 2 , 3 ❙
rule rules?AngleInvertible ❙
parallel: point ⟶ point ⟶ bool ❘ = [v,w] (∠ v w ≐ 0) ∨ (∠ v w ≐ pi_num) ❘ # 1 ∥ 2 ❙
orthogonal: point ⟶ point ⟶ bool ❘ = [v,w] < v ,w > ≐ 0 ❘ # 1 ⊥⊥ 2 ❙ // jbot ❙
rightangle: ℝ ⟶ bool ❘ = [x] x ≐ pi_num / 2 ❘ # ✓ 1❙ // jcheck ❙
// Lines ❙
line_type : type ❘ # line ❙
lineOf : point ⟶ point ⟶ line ❘ # from 1 to 2 ❙
basepoint : line ⟶ point ❘ # from 1 prec 1 ❙
targetpoint : line ⟶ point ❘ # to 1 prec 1 ❙
axiom_basepoint : {p1,p2} ⊦ from (from p1 to p2) ≐ p1 ❘ role ForwardRule ❙
axiom_targetpoint : {p1,p2} ⊦ to (from p1 to p2) ≐ p2 ❘ role ForwardRule ❙
lineDirection: line ⟶ point ❘ = [l] norm (( to l ) -- ( from l )) ❘ # dir 1 ❙ // wut? ❙
onLine : line ⟶ point ⟶ bool ❘ # 2 on 1 ❙ // definiens? ❙
sameLine: line ⟶ line ⟶ bool ❘ = [A ,B] ( (from B ) on A ) ∧ ( (lineDirection B) ∥ (lineDirection A) ) ❘ # 1 ≅ 2❙
intersect : line ⟶ line ⟶ bool ❘ = [A,B] ∃ [p] (p on A) ∧ (p on B) ∧ (¬ A ≅ B) ❘ # colL 1 2 ❙
pointOfIntersection : {A ,B } ( ⊦ colL A B ) ⟶ point ❘ # colLV 1 2 3 ❙
parallelLine: line ⟶ line ⟶ bool ❘ = [A,B] lineDirection A ∥ lineDirection B ❘ # paraL 1 2 ❙
pointOfIntersectionAxiom: {A, B, p} ⊦ ( ( colLV A B p) on A ) ∧ ( ( colLV A B p) on B) ❙
❚
theory Triangles > point : type,
addI : point ⟶ point ⟶ point,
subtractI : point ⟶ point ⟶ point,
multI : ℝ ⟶ point ⟶ point,
scpI : point ⟶ point ⟶ ℝ ❘ =
include (?Geometry/Common point addI subtractI multI scpI) ❙
triangle : type ❙
triangle_constructor : point ⟶ point ⟶ point ⟶ triangle ❘ # Δ 1 2 3 ❙
triangle_point1 : triangle ⟶ point ❘ # _A 1 prec 50 ❙
triangle_point2 : triangle ⟶ point ❘ # _B 1 prec 50 ❙
triangle_point3 : triangle ⟶ point ❘ # _C 1 prec 50 ❙
alpha_angle : triangle ⟶ ℝ ❘ # _α 1 prec 50 ❘ = [T] angle ( _B T -- _A T ) ( _C T -- _A T )❙
beta_angle : triangle ⟶ ℝ ❘ # _β 1 prec 50 ❘ = [T] angle ( _A T -- _B T ) ( _C T -- _B T )❙
gamma_angle : triangle ⟶ ℝ ❘ # _γ 1 prec 50 ❘ = [T] angle ( _A T -- _C T ) ( _B T -- _C T )❙
a_triangle: triangle ⟶ ℝ ❘ = [T] d- ( _B T) ( _C T) ❘ # _a 1 prec 50 ❙
b_triangle: triangle ⟶ ℝ ❘ = [T] d- ( _A T) ( _C T) ❘ # _b 1 prec 50 ❙
c_triangle: triangle ⟶ ℝ ❘ = [T] d- ( _A T) ( _B T) ❘ # _c 1 prec 50 ❙
height_triangle_basepoint_a: triangle ⟶ point ❘ # _haV 1 prec 50 ❙
height_triangle_basepoint_a_online_axiom: { T } ⊦ ( _haV T ) on ( from ( _B T) to ( _C T ) ) ❙
height_triangle_basepoint_a_orthogonal_axiom: { T } ⊦ ( _haV T -- _B T ) ⊥⊥ ( _haV T -- _A T ) ❙
ha_triangle_length: triangle ⟶ ℝ ❘ = [T] d- ( _A T ) ( _haV T )❘ # _ha 1 prec 50 ❙
height_triangle_basepoint_b: triangle ⟶ point ❘ # _hbV 1 prec 50 ❙
height_triangle_basepoint_b_online_axiom: { T } ⊦ ( _hbV T ) on ( from ( _A T) to ( _C T ) ) ❙
height_triangle_basepoint_b_orthogonal_axiom: { T } ⊦ ( _hbV T -- _A T ) ⊥⊥ ( _hbV T -- _B T ) ❙
hb_triangle_length: triangle ⟶ ℝ ❘ = [T] d- ( _B T ) ( _hbV T )❘ # _hb 1 prec 50 ❙
height_triangle_basepoint_c: triangle ⟶ point ❘ # _hcV 1 prec 50 ❙
height_triangle_basepoint_c_online_axiom: { T } ⊦ ( _hcV T ) on ( from ( _B T) to ( _A T ) ) ❙
height_triangle_basepoint_c_orthogonal_axiom: { T } ⊦ ( _hcV T -- _B T ) ⊥⊥ ( _hcV T -- _C T ) ❙
hc_triangle_length: triangle ⟶ ℝ ❘ = [T] d- ( _C T ) ( _hcV T )❘ # _hc 1 prec 50 ❙
lawOfCosine_Alpha: { T } ⊦ ( _a T ⋅ _a T ) ≐ ( _b T ⋅ _b T ) + ( _c T ⋅ _c T ) + 2 ⋅ _b T ⋅ _c T ⋅ ( cos ( _α T ) )❙
lawOfCosine_Beta : { T } ⊦ ( _b T ⋅ _b T ) ≐ ( _a T ⋅ _a T ) + ( _c T ⋅ _c T ) + 2 ⋅ _a T ⋅ _c T ⋅ ( cos ( _β T ) )❙
lawOfCosine_Gamma: { T } ⊦ ( _c T ⋅ _c T ) ≐ ( _a T ⋅ _a T ) + ( _b T ⋅ _b T ) + 2 ⋅ _a T ⋅ _b T ⋅ ( cos ( _γ T ) )❙
lawOfSinesAB: { T } ⊦ _a T / sin ( _α T ) ≐ _b T / sin ( _β T ) ❙
lawOfSinesAC: { T } ⊦ _a T / sin ( _α T ) ≐ _c T / sin ( _γ T ) ❙
lawOfSinesCB: { T } ⊦ _c T / sin ( _γ T ) ≐ _b T / sin ( _β T ) ❙
angleSum = {T} ⊦ (( _α T) + ( _β T) + ( _γ T) )≐ pi_num ❙
area: triangle ⟶ ℝ ❘ = [T] ( _hb T) ⋅ ( _b T) / 2 ❘ # AΔ 1 prec 1 ❙
❚
theory SymmetricTriangles > point : type,
addI : point ⟶ point ⟶ point,
subtractI : point ⟶ point ⟶ point,
multI : ℝ ⟶ point ⟶ point,
scpI : point ⟶ point ⟶ ℝ ❘ =
include (?Geometry/Triangles point addI subtractI multI scpI) ❙
symmetric_α: triangle ⟶ bool ❘ = [T] _β T ≐ _γ T ❘ # sym_α 1 ❙
symmetric_β: triangle ⟶ bool ❘ = [T] _α T ≐ _γ T ❘ # sym_β 1 ❙
symmetric_γ: triangle ⟶ 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 ❙
❚
theory RightTriangles > point : type,
addI : point ⟶ point ⟶ point,
subtractI : point ⟶ point ⟶ point,
multI : ℝ ⟶ point ⟶ point,
scpI : point ⟶ point ⟶ ℝ ❘ =
include (?Geometry/Triangles point addI subtractI multI scpI) ❙
pythagoras_alpha = [T] ( _c T) ⋅ ( _c T) + ( _b T) ⋅ ( _b T) ≐ ( _a T) ⋅ ( _a T) ❙
pythagoras_beta = [T] ( _a T) ⋅ ( _a T) + ( _c T) ⋅ ( _c T) ≐ ( _b T) ⋅ ( _b T) ❙
pythagoras_gamma = [T] ( _a T) ⋅ ( _a T) + ( _b T) ⋅ ( _b T) ≐ ( _c T) ⋅ ( _c T) ❙
right_alpha_prop = [T] ✓ _α T ❙
right_beta_prop = [T] ✓ _β T ❙
right_gamma_prop = [T] ✓ _γ T ❙
pythagoras_theorem_alpha : {T} { p : ⊦ right_alpha_prop T } ⊦ pythagoras_alpha T ❙
pythagoras_theorem_beta : {T} { p : ⊦ right_beta_prop T } ⊦ pythagoras_beta T ❙
pythagoras_theorem_gamma : {T} { p : ⊦ right_gamma_prop T } ⊦ pythagoras_gamma T ❙
geometric_mean_alpha = [T] ( _ha T ⋅ _ha T ) ≐ ( d- ( _haV T ) ( _B T ) ) ⋅ ( d- ( _haV T) ( _C T ) ) ❙
geometric_mean_beta = [T] ( _hb T ⋅ _hb T ) ≐ ( d- ( _hbV T ) ( _A T ) ) ⋅ ( d- ( _hbV T) ( _C T ) ) ❙
geometric_mean_gamma = [T] ( _hc T ⋅ _hc T ) ≐ ( d- ( _hcV T ) ( _B T ) ) ⋅ ( d- ( _hcV T) ( _A T ) ) ❙
geometric_mean_theorem_alpha : {T} { p : ⊦ ( ✓ _α T ) } ⊦ geometric_mean_alpha T ❙
geometric_mean_theorem_beta : {T} { p : ⊦ ( ✓ _β T ) } ⊦ geometric_mean_beta T ❙
geometric_mean_theorem_gamma : {T} { p : ⊦ ( ✓ _γ T ) } ⊦ geometric_mean_gamma T ❙
cathetus_alpha_1 = [T] ( _b T ⋅ _b T ) ≐ _a T ⋅ ( d- ( _haV T) ( _C T ) )❙
cathetus_alpha_2 = [T] ( _c T ⋅ _c T ) ≐ _a T ⋅ ( d- ( _haV T) ( _B T ) )❙
cathetus_beta_1 = [T] ( _c T ⋅ _c T ) ≐ _b T ⋅ ( d- ( _hbV T) ( _A T ) )❙
cathetus_beta_2 = [T] ( _a T ⋅ _a T ) ≐ _b T ⋅ ( d- ( _hbV T) ( _C T ) )❙
cathetus_gamma_1 = [T] ( _a T ⋅ _a T ) ≐ _c T ⋅ ( d- ( _hcV T) ( _B T ) )❙
cathetus_gamma_2 = [T] ( _b T ⋅ _b T ) ≐ _c T ⋅ ( d- ( _hcV T) ( _A T ) )❙
catheus_theorem_alpha_1 : {T} { p : ⊦ ( ✓ _α T ) } ⊦ cathetus_alpha_1 T ❙
catheus_theorem_alpha_2 : {T} { p : ⊦ ( ✓ _α T ) } ⊦ cathetus_alpha_2 T ❙
catheus_theorem_beta_1 : {T} { p : ⊦ ( ✓ _β T ) } ⊦ cathetus_beta_1 T ❙
catheus_theorem_beta_2 : {T} { p : ⊦ ( ✓ _β T ) } ⊦ cathetus_beta_2 T ❙
catheus_theorem_gamma_1 : {T} { p : ⊦ ( ✓ _γ T ) } ⊦ cathetus_gamma_1 T ❙
catheus_theorem_gamma_2 : {T} { p : ⊦ ( ✓ _γ T ) } ⊦ cathetus_gamma_2 T ❙
❚
❚