Equations
- EuclidGeom.divratio A B C = (EuclidGeom.Vec.mkPtPt A B / EuclidGeom.Vec.mkPtPt A C).re
Instances For
theorem
EuclidGeom.ratio_is_real'
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
(C : P)
(colin : EuclidGeom.Collinear A B C)
[cnea : EuclidGeom.PtNe C A]
:
(EuclidGeom.Vec.mkPtPt A B / EuclidGeom.Vec.mkPtPt A C).im = 0
theorem
EuclidGeom.ratio_is_real
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
(C : P)
(colin : EuclidGeom.Collinear A B C)
[cnea : EuclidGeom.PtNe C A]
:
EuclidGeom.Vec.mkPtPt A B / EuclidGeom.Vec.mkPtPt A C = ↑(EuclidGeom.divratio A B C)
theorem
EuclidGeom.vec_eq_vec_smul_ratio
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
(C : P)
(colin : EuclidGeom.Collinear A B C)
[cnea : EuclidGeom.PtNe C A]
:
EuclidGeom.Vec.mkPtPt A B = EuclidGeom.divratio A B C • EuclidGeom.Vec.mkPtPt A C
theorem
EuclidGeom.ratio_eq_ratio_div_ratio_minus_one
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
(C : P)
[cnea : EuclidGeom.PtNe C A]
(colin : EuclidGeom.Collinear A B C)
:
EuclidGeom.divratio B A C = EuclidGeom.divratio A B C / (EuclidGeom.divratio A B C - 1)
theorem
EuclidGeom.pt_eq_of_ratio_eq_of_ne_ne
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
(C : P)
(D : P)
[cned : EuclidGeom.PtNe C D]
[dnea : EuclidGeom.PtNe D A]
[dneb : EuclidGeom.PtNe D B]
(colinacd : EuclidGeom.Collinear A C D)
(colinbcd : EuclidGeom.Collinear B C D)
(req : EuclidGeom.divratio A C D = EuclidGeom.divratio B C D)
:
A = B
theorem
EuclidGeom.ratio_eq_zero_of_point_eq1
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
:
EuclidGeom.divratio A A B = 0
theorem
EuclidGeom.ratio_eq_zero_of_point_eq2
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
:
EuclidGeom.divratio A B A = 0