theorem
EuclidGeom.DirLine.ne_iff_ne_as_line_elem
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
:
A ≠ B ↔ EuclidGeom.DirLine.lelem A ha ≠ EuclidGeom.DirLine.lelem B hb
theorem
EuclidGeom.DirLine.exist_pos_smul_of_lt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(a_lt_b : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb)
:
theorem
EuclidGeom.DirLine.exist_nonneg_smul_of_le
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(a_le_b : EuclidGeom.DirLine.lelem A ha ≤ EuclidGeom.DirLine.lelem B hb)
:
theorem
EuclidGeom.DirLine.lt_of_exist_pos_smul
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(h : ∃ (x : ℝ), 0 < x ∧ EuclidGeom.Vec.mkPtPt A B = x • Dl.toDir.unitVec)
:
theorem
EuclidGeom.DirLine.le_of_exist_nonneg_smul
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(h : ∃ (x : ℝ), 0 ≤ x ∧ EuclidGeom.Vec.mkPtPt A B = x • Dl.toDir.unitVec)
:
theorem
EuclidGeom.DirLine.lies_int_seg_nd_ext_iff_lies_int
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
(C : P)
[a_ne_c : EuclidGeom.PtNe A C]
:
EuclidGeom.lies_int B (EuclidGeom.SegND.extension (SEG_nd A C)) ↔ EuclidGeom.lies_int C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_on_seg_nd_ext_iff_lies_on
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
(C : P)
[a_ne_c : EuclidGeom.PtNe A C]
:
EuclidGeom.lies_on B (EuclidGeom.SegND.extension (SEG_nd A C)) ↔ EuclidGeom.lies_on C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_int_seg_of_lt_and_lt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_lt_b : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb)
(b_lt_c : EuclidGeom.DirLine.lelem B hb < EuclidGeom.DirLine.lelem C hc)
:
EuclidGeom.lies_int B { source := A, target := C }
theorem
EuclidGeom.DirLine.lies_int_seg_of_gt_and_gt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_gt_b : EuclidGeom.DirLine.lelem A ha > EuclidGeom.DirLine.lelem B hb)
(b_gt_c : EuclidGeom.DirLine.lelem B hb > EuclidGeom.DirLine.lelem C hc)
:
EuclidGeom.lies_int B { source := A, target := C }
theorem
EuclidGeom.DirLine.lies_on_seg_of_le_and_le
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_le_b : EuclidGeom.DirLine.lelem A ha ≤ EuclidGeom.DirLine.lelem B hb)
(b_le_c : EuclidGeom.DirLine.lelem B hb ≤ EuclidGeom.DirLine.lelem C hc)
:
EuclidGeom.lies_on B { source := A, target := C }
theorem
EuclidGeom.DirLine.lies_on_seg_of_ge_and_ge
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_ge_b : EuclidGeom.DirLine.lelem A ha ≥ EuclidGeom.DirLine.lelem B hb)
(b_ge_c : EuclidGeom.DirLine.lelem B hb ≥ EuclidGeom.DirLine.lelem C hc)
:
EuclidGeom.lies_on B { source := A, target := C }
theorem
EuclidGeom.DirLine.eq_toDir_of_lt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(a_lt_b : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb)
:
theorem
EuclidGeom.DirLine.neg_toDir_of_gt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(a_gt_b : EuclidGeom.DirLine.lelem A ha > EuclidGeom.DirLine.lelem B hb)
:
theorem
EuclidGeom.DirLine.lies_int_ray_of_lt_and_lt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_lt_b : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb)
(a_lt_c : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem C hc)
:
EuclidGeom.lies_int B (RAY A C (_ : C ≠ A))
theorem
EuclidGeom.DirLine.lies_int_ray_of_gt_and_gt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_gt_b : EuclidGeom.DirLine.lelem A ha > EuclidGeom.DirLine.lelem B hb)
(a_gt_c : EuclidGeom.DirLine.lelem A ha > EuclidGeom.DirLine.lelem C hc)
:
EuclidGeom.lies_int B (RAY A C (_ : C ≠ A))
theorem
EuclidGeom.DirLine.lies_on_ray_of_le_and_lt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_le_b : EuclidGeom.DirLine.lelem A ha ≤ EuclidGeom.DirLine.lelem B hb)
(a_lt_c : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem C hc)
:
EuclidGeom.lies_on B (RAY A C (_ : C ≠ A))
theorem
EuclidGeom.DirLine.lies_on_ray_of_ge_and_gt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_ge_b : EuclidGeom.DirLine.lelem A ha ≥ EuclidGeom.DirLine.lelem B hb)
(a_gt_c : EuclidGeom.DirLine.lelem A ha > EuclidGeom.DirLine.lelem C hc)
:
EuclidGeom.lies_on B (RAY A C (_ : C ≠ A))
theorem
EuclidGeom.DirLine.lies_int_seg_nd_ext_of_lt_and_lt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_lt_c : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem C hc)
(c_lt_b : EuclidGeom.DirLine.lelem C hc < EuclidGeom.DirLine.lelem B hb)
:
EuclidGeom.lies_int B (EuclidGeom.SegND.extension (SEG_nd A C (_ : C ≠ A)))
theorem
EuclidGeom.DirLine.lies_int_seg_nd_ext_of_gt_and_gt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_gt_c : EuclidGeom.DirLine.lelem A ha > EuclidGeom.DirLine.lelem C hc)
(c_gt_b : EuclidGeom.DirLine.lelem C hc > EuclidGeom.DirLine.lelem B hb)
:
EuclidGeom.lies_int B (EuclidGeom.SegND.extension (SEG_nd A C (_ : C ≠ A)))
theorem
EuclidGeom.DirLine.lies_on_seg_nd_ext_of_lt_and_le
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_lt_c : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem C hc)
(c_le_b : EuclidGeom.DirLine.lelem C hc ≤ EuclidGeom.DirLine.lelem B hb)
:
EuclidGeom.lies_on B (EuclidGeom.SegND.extension (SEG_nd A C (_ : C ≠ A)))
theorem
EuclidGeom.DirLine.lies_on_seg_nd_ext_of_gt_and_ge
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(a_gt_c : EuclidGeom.DirLine.lelem A ha > EuclidGeom.DirLine.lelem C hc)
(c_ge_b : EuclidGeom.DirLine.lelem C hc ≥ EuclidGeom.DirLine.lelem B hb)
:
EuclidGeom.lies_on B (EuclidGeom.SegND.extension (SEG_nd A C (_ : C ≠ A)))
theorem
EuclidGeom.DirLine.lt_and_lt_of_lies_int_seg_and_le
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(hac : EuclidGeom.lies_int B { source := A, target := C })
(a_le_c : EuclidGeom.DirLine.lelem A ha ≤ EuclidGeom.DirLine.lelem C hc)
:
EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb ∧ EuclidGeom.DirLine.lelem B hb < EuclidGeom.DirLine.lelem C hc
theorem
EuclidGeom.DirLine.ord_of_lies_int_seg
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(hac : EuclidGeom.lies_int B { source := A, target := C })
:
EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb ∧ EuclidGeom.DirLine.lelem B hb < EuclidGeom.DirLine.lelem C hc ∨ EuclidGeom.DirLine.lelem A ha > EuclidGeom.DirLine.lelem B hb ∧ EuclidGeom.DirLine.lelem B hb > EuclidGeom.DirLine.lelem C hc
theorem
EuclidGeom.DirLine.lt_iff_lt_of_lies_int_seg₁₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(hac : EuclidGeom.lies_int B { source := A, target := C })
:
EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb ↔ EuclidGeom.DirLine.lelem B hb < EuclidGeom.DirLine.lelem C hc
theorem
EuclidGeom.DirLine.lt_iff_lt_of_lies_int_seg₁₂
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(hac : EuclidGeom.lies_int B { source := A, target := C })
:
EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb ↔ EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem C hc
theorem
EuclidGeom.DirLine.lt_iff_lt_of_lies_int_seg₂₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(hac : EuclidGeom.lies_int B { source := A, target := C })
:
EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem C hc ↔ EuclidGeom.DirLine.lelem B hb < EuclidGeom.DirLine.lelem C hc
theorem
EuclidGeom.DirLine.le_and_le_of_lies_on_seg_and_le
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(hac : EuclidGeom.lies_on B { source := A, target := C })
(a_le_c : EuclidGeom.DirLine.lelem A ha ≤ EuclidGeom.DirLine.lelem C hc)
:
EuclidGeom.DirLine.lelem A ha ≤ EuclidGeom.DirLine.lelem B hb ∧ EuclidGeom.DirLine.lelem B hb ≤ EuclidGeom.DirLine.lelem C hc
theorem
EuclidGeom.DirLine.ord_of_lies_on_seg
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(h : EuclidGeom.lies_on B { source := A, target := C })
:
EuclidGeom.DirLine.lelem A ha ≤ EuclidGeom.DirLine.lelem B hb ∧ EuclidGeom.DirLine.lelem B hb ≤ EuclidGeom.DirLine.lelem C hc ∨ EuclidGeom.DirLine.lelem A ha ≥ EuclidGeom.DirLine.lelem B hb ∧ EuclidGeom.DirLine.lelem B hb ≥ EuclidGeom.DirLine.lelem C hc
theorem
EuclidGeom.DirLine.le_of_lies_on_seg_and_lt₃₁
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(h : EuclidGeom.lies_on B { source := A, target := C })
(h1 : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb)
:
theorem
EuclidGeom.DirLine.lt_of_lies_on_seg_and_lt₂₁
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(h : EuclidGeom.lies_on B { source := A, target := C })
(h1 : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb)
:
theorem
EuclidGeom.DirLine.le_of_lies_on_seg_and_lt₁₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(h : EuclidGeom.lies_on B { source := A, target := C })
(h3 : EuclidGeom.DirLine.lelem B hb < EuclidGeom.DirLine.lelem C hc)
:
theorem
EuclidGeom.DirLine.lt_of_lies_on_seg_and_lt₂₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(h : EuclidGeom.lies_on B { source := A, target := C })
(h3 : EuclidGeom.DirLine.lelem B hb < EuclidGeom.DirLine.lelem C hc)
:
theorem
EuclidGeom.DirLine.le_of_lies_on_seg_and_le₁₂
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(h : EuclidGeom.lies_on B { source := A, target := C })
(h2 : EuclidGeom.DirLine.lelem A ha ≤ EuclidGeom.DirLine.lelem C hc)
:
theorem
EuclidGeom.DirLine.le_of_lies_on_seg_and_le₃₂
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(h : EuclidGeom.lies_on B { source := A, target := C })
(h2 : EuclidGeom.DirLine.lelem A ha ≤ EuclidGeom.DirLine.lelem C hc)
:
theorem
EuclidGeom.DirLine.lt_iff_lt_of_lies_int_ray
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
[hh : EuclidGeom.PtNe A C]
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(h : EuclidGeom.lies_int B (RAY A C))
:
EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem C hc ↔ EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb
theorem
EuclidGeom.DirLine.lt_of_lies_on_ray_and_lt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
[hh : EuclidGeom.PtNe A C]
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(h : EuclidGeom.lies_on B (RAY A C))
(h1 : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb)
:
theorem
EuclidGeom.DirLine.le_of_lies_on_ray_and_lt
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
[hh : EuclidGeom.PtNe A C]
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
(h : EuclidGeom.lies_on B (RAY A C))
(h1 : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem C hc)
:
theorem
EuclidGeom.DirLine.lt_of_eq_toDir
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
[a_ne_b : EuclidGeom.PtNe A B]
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(h : (RAY A B).toDir = Dl.toDir)
:
theorem
EuclidGeom.DirLine.gt_of_neg_toDir
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
[a_ne_b : EuclidGeom.PtNe A B]
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(h : (RAY A B).toDir = -Dl.toDir)
:
theorem
EuclidGeom.DirLine.lies_on_or_lies_on_or_lies_on_of_lies_on_DirLine
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
:
EuclidGeom.lies_on A { source := B, target := C } ∨ EuclidGeom.lies_on B { source := A, target := C } ∨ EuclidGeom.lies_on C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_on_or_lies_on_or_lies_on_of_lies_on_Line
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
(ha : EuclidGeom.lies_on A l)
(hb : EuclidGeom.lies_on B l)
(hc : EuclidGeom.lies_on C l)
:
EuclidGeom.lies_on A { source := B, target := C } ∨ EuclidGeom.lies_on B { source := A, target := C } ∨ EuclidGeom.lies_on C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_on_or_lies_on_or_lies_on_of_collinear
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
(h : EuclidGeom.Collinear A B C)
:
EuclidGeom.lies_on A { source := B, target := C } ∨ EuclidGeom.lies_on B { source := A, target := C } ∨ EuclidGeom.lies_on C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_int_or_lies_int_or_lies_int_of_lies_on_DirLine
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
:
EuclidGeom.lies_int A { source := B, target := C } ∨ EuclidGeom.lies_int B { source := A, target := C } ∨ EuclidGeom.lies_int C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_int_or_lies_int_or_lies_int_of_lies_on_Line
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(ha : EuclidGeom.lies_on A l)
(hb : EuclidGeom.lies_on B l)
(hc : EuclidGeom.lies_on C l)
:
EuclidGeom.lies_int A { source := B, target := C } ∨ EuclidGeom.lies_int B { source := A, target := C } ∨ EuclidGeom.lies_int C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_int_or_lies_int_or_lies_int_of_collinear
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(h : EuclidGeom.Collinear A B C)
:
EuclidGeom.lies_int A { source := B, target := C } ∨ EuclidGeom.lies_int B { source := A, target := C } ∨ EuclidGeom.lies_int C { source := A, target := B }
theorem
EuclidGeom.DirLine.not_lies_int_and_lies_int₁
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
(C : P)
:
¬(EuclidGeom.lies_int B { source := A, target := C } ∧ EuclidGeom.lies_int C { source := A, target := B })
theorem
EuclidGeom.DirLine.not_lies_int_and_lies_int₂
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
(C : P)
:
¬(EuclidGeom.lies_int A { source := B, target := C } ∧ EuclidGeom.lies_int C { source := A, target := B })
theorem
EuclidGeom.DirLine.not_lies_int_and_lies_int₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
(A : P)
(B : P)
(C : P)
:
¬(EuclidGeom.lies_int A { source := B, target := C } ∧ EuclidGeom.lies_int B { source := A, target := C })
theorem
EuclidGeom.DirLine.lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_DirLine₁
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
:
EuclidGeom.lies_int A { source := B, target := C } ↔ ¬EuclidGeom.lies_int B { source := A, target := C } ∧ ¬EuclidGeom.lies_int C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_DirLine₂
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
:
EuclidGeom.lies_int B { source := A, target := C } ↔ ¬EuclidGeom.lies_int A { source := B, target := C } ∧ ¬EuclidGeom.lies_int C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_DirLine₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{Dl : EuclidGeom.DirLine P}
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(ha : EuclidGeom.lies_on A Dl)
(hb : EuclidGeom.lies_on B Dl)
(hc : EuclidGeom.lies_on C Dl)
:
EuclidGeom.lies_int C { source := A, target := B } ↔ ¬EuclidGeom.lies_int A { source := B, target := C } ∧ ¬EuclidGeom.lies_int B { source := A, target := C }
theorem
EuclidGeom.DirLine.lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_Line₁
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(ha : EuclidGeom.lies_on A l)
(hb : EuclidGeom.lies_on B l)
(hc : EuclidGeom.lies_on C l)
:
EuclidGeom.lies_int A { source := B, target := C } ↔ ¬EuclidGeom.lies_int B { source := A, target := C } ∧ ¬EuclidGeom.lies_int C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_Line₂
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(ha : EuclidGeom.lies_on A l)
(hb : EuclidGeom.lies_on B l)
(hc : EuclidGeom.lies_on C l)
:
EuclidGeom.lies_int B { source := A, target := C } ↔ ¬EuclidGeom.lies_int A { source := B, target := C } ∧ ¬EuclidGeom.lies_int C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_int_iff_not_lies_int_and_not_lies_int_of_lies_on_Line₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{l : EuclidGeom.Line P}
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(ha : EuclidGeom.lies_on A l)
(hb : EuclidGeom.lies_on B l)
(hc : EuclidGeom.lies_on C l)
:
EuclidGeom.lies_int C { source := A, target := B } ↔ ¬EuclidGeom.lies_int A { source := B, target := C } ∧ ¬EuclidGeom.lies_int B { source := A, target := C }
theorem
EuclidGeom.DirLine.lies_int_iff_not_lies_int_and_not_lies_int_of_collinear₁
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(h : EuclidGeom.Collinear A B C)
:
EuclidGeom.lies_int A { source := B, target := C } ↔ ¬EuclidGeom.lies_int B { source := A, target := C } ∧ ¬EuclidGeom.lies_int C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_int_iff_not_lies_int_and_not_lies_int_of_collinear₂
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(h : EuclidGeom.Collinear A B C)
:
EuclidGeom.lies_int B { source := A, target := C } ↔ ¬EuclidGeom.lies_int A { source := B, target := C } ∧ ¬EuclidGeom.lies_int C { source := A, target := B }
theorem
EuclidGeom.DirLine.lies_int_iff_not_lies_int_and_not_lies_int_of_collinear₃
{P : Type u_1}
[EuclidGeom.EuclideanPlane P]
{A : P}
{B : P}
{C : P}
[hh1 : EuclidGeom.PtNe A B]
[hh2 : EuclidGeom.PtNe A C]
[hh3 : EuclidGeom.PtNe B C]
(h : EuclidGeom.Collinear A B C)
:
EuclidGeom.lies_int C { source := A, target := B } ↔ ¬EuclidGeom.lies_int A { source := B, target := C } ∧ ¬EuclidGeom.lies_int B { source := A, target := C }