def EuclidGeom.collinear_of_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [_hac : EuclidGeom.PtNe A C] [_hba : EuclidGeom.PtNe B A] : Prop

Given three distinct (ordered) points $A$, $B$, $C$, this function returns whether they are collinear, i.e. whether the projective direction of the vector $\overrightarrow{AB}$ is the same as the projective direction of the vector $\overrightarrow{AC}$.

Equations

• EuclidGeom.collinear_of_nd = ((VEC_nd A B (_ : B ≠ A)).toProj = (VEC_nd A C (_ : C ≠ A)).toProj)

def EuclidGeom.Collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : Prop

Given three points $A$, $B$, $C$, return whether they are collinear: if at least two of them are equal, then they are considered collinear; if the three points are distinct, we use the earlier definition of colinarity for distinct points.

Equations

• EuclidGeom.Collinear A B C = if h : C = B ∨ A = C ∨ B = A then True else EuclidGeom.collinear_of_nd

theorem EuclidGeom.collinear_of_vec_eq_smul_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {t : ℝ} (e : EuclidGeom.Vec.mkPtPt A C = t • EuclidGeom.Vec.mkPtPt A B) : EuclidGeom.Collinear A B C

Given three points $A$, $B$, $C$ and a real number $t$, if the vector $\overrightarrow{AC}$ is $t$ times the vector $\overrightarrow{AB}$, then $A$, $B$, and $C$ are collinear.

theorem EuclidGeom.collinear_of_vec_eq_smul_vec' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} : (∃ (t : ℝ), EuclidGeom.Vec.mkPtPt A C = t • EuclidGeom.Vec.mkPtPt A B) → EuclidGeom.Collinear A B C

Given three points $A$, $B$, $C$, if the vector $\overrightarrow{AC}$ is a scalar multiple of the vector $\overrightarrow{AB}$, then $A$, $B$, $C$ are collinear.

theorem EuclidGeom.collinear_iff_eq_smul_vec_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [g : EuclidGeom.PtNe B A] : EuclidGeom.Collinear A B C ↔ ∃ (r : ℝ), EuclidGeom.Vec.mkPtPt A C = r • EuclidGeom.Vec.mkPtPt A B

Given three points $A$, $B$, $C$ such that $B \neq A$, we have $A$, $B$, $C$ are collinear if and only if the vector $\overrightarrow{AC}$ is a scalar multiple of the vector $\overrightarrow{AB}$.

theorem EuclidGeom.triv_collinear₁₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (C : P) : EuclidGeom.Collinear A A C

For any two points $A$ and $C$, the points $A$, $A$, $C$ are collinear.

theorem EuclidGeom.collinear_of_trd_eq_snd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) {B : P} {C : P} (h : C = B) : EuclidGeom.Collinear A B C

theorem EuclidGeom.collinear_of_fst_eq_snd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (B : P) {A : P} {C : P} (h : A = C) : EuclidGeom.Collinear A B C

theorem EuclidGeom.collinear_of_snd_eq_fst {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} (C : P) (h : B = A) : EuclidGeom.Collinear A B C

theorem EuclidGeom.Collinear.perm₁₃₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (c : EuclidGeom.Collinear A B C) : EuclidGeom.Collinear A C B

Given three points $A$, $B$, and $C$, if $A$, $B$, $C$ are collinear (in that order), then $A$, $C$, $B$ are collinear (in that order); in other words, swapping the last two of the three points does not change the definition of colinarity.

theorem EuclidGeom.Collinear.perm₂₁₃ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (c : EuclidGeom.Collinear A B C) : EuclidGeom.Collinear B A C

Given three points $A$, $B$, and $C$, if $A$, $B$, $C$ are collinear (in that order), then $B$, $A$, $C$ are collinear (in that order); in other words, in the definition of colinarity, swapping the first two of the three points does not change property of the three points being collinear.

theorem EuclidGeom.Collinear.perm₂₃₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (h : EuclidGeom.Collinear A B C) : EuclidGeom.Collinear B C A

theorem EuclidGeom.Collinear.perm₃₁₂ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (h : EuclidGeom.Collinear A B C) : EuclidGeom.Collinear C A B

theorem EuclidGeom.Collinear.perm₃₂₁ {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (h : EuclidGeom.Collinear A B C) : EuclidGeom.Collinear C B A

theorem EuclidGeom.collinear_of_collinear_collinear_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {D : P} (h₁ : EuclidGeom.Collinear A B C) (h₂ : EuclidGeom.Collinear A B D) [h : EuclidGeom.PtNe B A] : EuclidGeom.Collinear A C D

Given four points $A$, $B$, $C$, $D$ with $B \neq A$, if $A$, $B$, $C$ are collinear, and if $A$, $B$, $D$ are collinear, then $A$, $C$, $D$ are collinear.

theorem EuclidGeom.ne_of_not_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (h : ¬EuclidGeom.Collinear A B C) : C ≠ B ∧ A ≠ C ∧ B ≠ A

Given three points $A$, $B$, $C$, if they are not collinear, then they are pairwise distinct, i.e. $C \neq B$, $A \neq C$, and $B \neq A$.

theorem EuclidGeom.collinear_iff_toProj_eq_of_ptNe {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [hba : EuclidGeom.PtNe B A] [hca : EuclidGeom.PtNe C A] : EuclidGeom.Collinear A B C ↔ (VEC_nd A B).toProj = (VEC_nd A C).toProj

theorem EuclidGeom.Ray.collinear_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {ray : EuclidGeom.Ray P} (hA : EuclidGeom.lies_on A ray) (hB : EuclidGeom.lies_on B ray) (hC : EuclidGeom.lies_on C ray) : EuclidGeom.Collinear A B C

If $A$, $B$, $C$ are three points which lie on a ray, then they are collinear.

theorem EuclidGeom.Seg.collinear_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} {seg : EuclidGeom.Seg P} (hA : EuclidGeom.lies_on A seg) (hB : EuclidGeom.lies_on B seg) (hC : EuclidGeom.lies_on C seg) : EuclidGeom.Collinear A B C

If $A$, $B$, $C$ are three points which lie on a segment, then they are collinear.

theorem EuclidGeom.nontriv_of_plane {H : Type u_2} [h : EuclidGeom.EuclideanPlane H] : ∃ (A : H) (B : H) (C : H), ¬EuclidGeom.Collinear A B C

There exists three points $A$, $B$, $C$ on the plane such that they are not collinear.