def EuclidGeom.same_dir_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.Ray P → EuclidGeom.Ray P → Prop

We say that rays $r$ and $r'$ \emph{induce the same directed line} if, (1) they have the same direction, and (2) the source of $r'$ lies on $r$ or the reverse range of $r$.

Equations

• EuclidGeom.same_dir_line r r' = (r.toDir = r'.toDir ∧ (EuclidGeom.lies_on r'.source r ∨ EuclidGeom.lies_on r'.source r.reverse))

theorem EuclidGeom.same_dir_line.refl {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) : EuclidGeom.same_dir_line r r

Rays $r$ and $r$ induce the same directed line.

theorem EuclidGeom.same_dir_line.symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {r' : EuclidGeom.Ray P} (h : EuclidGeom.same_dir_line r r') : EuclidGeom.same_dir_line r' r

If $r$ and $r'$ induce the same directed line, then $r'$ and $r$ induce the same directed line.

theorem EuclidGeom.same_dir_line.trans {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {r' : EuclidGeom.Ray P} {r'' : EuclidGeom.Ray P} (h₁ : EuclidGeom.same_dir_line r r') (h₂ : EuclidGeom.same_dir_line r' r'') : EuclidGeom.same_dir_line r r''

If $r$, $r'$, and $r''$ are rays such that $r$ and $r'$ induce the same directed line, and $r'$ and $r''$ induce the same directed line, then $r$ and $r''$ induce the same directed line.

def EuclidGeom.same_dir_line.setoid {P : Type u_1} [EuclidGeom.EuclideanPlane P] : Setoid (EuclidGeom.Ray P)

Define an equivalence relation of rays with the same directed line, consisting of reflexive, symmetric, and transitivity conditions.

Equations

• EuclidGeom.same_dir_line.setoid = { r := EuclidGeom.same_dir_line, iseqv := (_ : Equivalence EuclidGeom.same_dir_line) }

def EuclidGeom.same_extn_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.Ray P → EuclidGeom.Ray P → Prop

We say two rays $r$ and $r'$ \emph{have the same extension line} if, (1) they have the same projective direction, and (2) if the sourse of $r'$ lies either on $r$ or the reverse ray of $r$.

Equations

• EuclidGeom.same_extn_line r r' = (r.toProj = r'.toProj ∧ (EuclidGeom.lies_on r'.source r ∨ EuclidGeom.lies_on r'.source r.reverse))

theorem EuclidGeom.same_extn_line.dir_eq_or_eq_neg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {r' : EuclidGeom.Ray P} (h : EuclidGeom.same_extn_line r r') : r.toDir = r'.toDir ∨ r.toDir = -r'.toDir

If two rays $r$ and $r'$ have the same extension line, then either they have the same direction or opposite direction.

theorem EuclidGeom.same_extn_line.vec_parallel_of_same_extn_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {r' : EuclidGeom.Ray P} (h : EuclidGeom.same_extn_line r r') : ∃ (t : ℝ), r'.toDir.unitVec = t • r.toDir.unitVec

If two rays $r$ and $r'$ have the same extension line, then the unit vector determined by $r'$ is some real multiple of the unit vecgtor determined by $r$.

theorem EuclidGeom.same_extn_line.ray_rev_of_same_extn_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} : EuclidGeom.same_extn_line r r.reverse

The reverse of a ray have the same extension line as the ray.

theorem EuclidGeom.same_extn_line.pt_pt_ray_same_extn_line_of_pt_pt_lies_on_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {r : EuclidGeom.Ray P} [_h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A r ∨ EuclidGeom.lies_on A r.reverse) (hb : EuclidGeom.lies_on B r ∨ EuclidGeom.lies_on B r.reverse) : EuclidGeom.same_extn_line r (RAY A B)

For two distinct points $A$ and $B$, if $A$ lies on a ray $r$ or its reverse ray and $B$ also lies on $r$ or its reverse ray, then the ray $r$ and the ray $\overline{AB}$ have the same extension line.

theorem EuclidGeom.same_extn_line.refl {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) : EuclidGeom.same_extn_line r r

A ray $r$ has the same extension line as itself.

theorem EuclidGeom.same_extn_line.symm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {r' : EuclidGeom.Ray P} (h : EuclidGeom.same_extn_line r r') : EuclidGeom.same_extn_line r' r

The symmetric property of same_extn_line. It states that if two rays $r$ and $r'$ have the same extension line, then $r'$ and $r$ also have the same extension line.

theorem EuclidGeom.same_extn_line.trans {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {r' : EuclidGeom.Ray P} {r'' : EuclidGeom.Ray P} (h₁ : EuclidGeom.same_extn_line r r') (h₂ : EuclidGeom.same_extn_line r' r'') : EuclidGeom.same_extn_line r r''

The transitivity of the same extension line relation. If $r$, $r'$, and $r''$ are rays such that $r$ and $r'$ have the same extension line, and $r'$ and $r''$ have the same extension line, then $r$ and $r''$ have the same extension line.

def EuclidGeom.same_extn_line.setoid {P : Type u_1} [EuclidGeom.EuclideanPlane P] : Setoid (EuclidGeom.Ray P)

Equations

• EuclidGeom.same_extn_line.setoid = { r := EuclidGeom.same_extn_line, iseqv := (_ : Equivalence EuclidGeom.same_extn_line) }

theorem EuclidGeom.same_extn_line_of_PM {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) {x : EuclidGeom.Dir} {y : EuclidGeom.Dir} (h : x = y ∨ x = -y) : EuclidGeom.same_extn_line { source := A, toDir := x } { source := A, toDir := y }

Given two directions, either the same or opposite, the rays starting from a same point with the two directions have the same extension line.

theorem EuclidGeom.same_extn_line.subset_carrier_union_rev_carrier {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {r' : EuclidGeom.Ray P} (h : EuclidGeom.same_extn_line r r') : EuclidGeom.Ray.carrier r' ∪ EuclidGeom.Ray.carrier r'.reverse ⊆ EuclidGeom.Ray.carrier r ∪ EuclidGeom.Ray.carrier r.reverse

If two rays $r$ and $r'$ have the same extension lines, then the union of the set of $r'$ and its reverse is contained in the union of the set of $r$ and its reverse.

theorem EuclidGeom.same_extn_line.eq_carrier_union_rev_carrier {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) (r' : EuclidGeom.Ray P) (h : EuclidGeom.same_extn_line r r') : EuclidGeom.Ray.carrier r ∪ EuclidGeom.Ray.carrier r.reverse = EuclidGeom.Ray.carrier r' ∪ EuclidGeom.Ray.carrier r'.reverse

If two rays $r$ and $r'$ have the same extension lines, then the union of the set of $r'$ and its reverse is the same as the union of the set of $r$ and its reverse.

theorem EuclidGeom.same_dir_line_le_same_extn_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.same_dir_line.setoid ≤ EuclidGeom.same_extn_line.setoid

This theorem gives the relation between two equivalence relations: having the same directed line implies having the same extension line.

def EuclidGeom.DirLine (P : Type u_1) [EuclidGeom.EuclideanPlane P] : Type u_1

A \emph{directed line} is the equivalence class of rays with the same directed lines.

Equations

• EuclidGeom.DirLine P = Quotient EuclidGeom.same_dir_line.setoid

def EuclidGeom.Line (P : Type u_1) [EuclidGeom.EuclideanPlane P] : Type u_1

A \emph{line} is the equivalence class of rays with the same exetnsion lines.

Equations

• EuclidGeom.Line P = Quotient EuclidGeom.same_extn_line.setoid

def EuclidGeom.DirLine.mk_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (h : B ≠ A) : EuclidGeom.DirLine P

Given two distinct points $A$ and $B$, this function returns the directed line starting from $A$ in the direction of $B$. We use $\verb|DLIN| A B$ or $\verb|DLIN| A B h$ to abbreviate $\verb|DLine.mk_pt_pt| A B h$, where $h$ is a statement that $A \neq B$. When such statement $h$ is missing, we search it in all the known facts.

Equations

• DLIN A B h = ⟦RAY A B h⟧

def EuclidGeom.DirLine.mk_pt_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (dir : EuclidGeom.Dir) : EuclidGeom.DirLine P

Given a point $A$ and a direction, this function returns the directed line starting from $A$ in the given direction.

Equations

• EuclidGeom.DirLine.mk_pt_dir A dir = ⟦{ source := A, toDir := dir }⟧

def EuclidGeom.DirLine.mk_pt_vec_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (vec_nd : EuclidGeom.VecND) : EuclidGeom.DirLine P

Given a point $A$ and a nondegenerate vector, this function returns the directed line starting from $A$ in the same direction of the nondegenerate vector.

Equations

• EuclidGeom.DirLine.mk_pt_vec_nd A vec_nd = EuclidGeom.DirLine.mk_pt_dir A vec_nd.toDir

def EuclidGeom.Line.mk_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (h : B ≠ A) : EuclidGeom.Line P

Given two distinct points $A$ and $B$, this function returns the line passing through $A$ and $B$. We use $\verb|LIN| A B$ or $\verb|LIN| A B h$ to abbreviate $\verb|Line.mk_pt_pt| A B h$, where $h$ is a statement that $A \neq B$. When such statement $h$ is missing, we search it in all the known facts.

Equations

• LIN A B h = ⟦RAY A B h⟧

def EuclidGeom.Line.mk_pt_proj {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (proj : EuclidGeom.Proj) : EuclidGeom.Line P

Given a point $A$ and a projective direction, this function returns the line through $A$ along the given projective direction.

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.Line.mk_pt_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (dir : EuclidGeom.Dir) : EuclidGeom.Line P

Given a point $A$ and a direction, this function returns the line through $A$ along the given direction.

Equations

• EuclidGeom.Line.mk_pt_dir A dir = EuclidGeom.Line.mk_pt_proj A dir.toProj

@[simp]

theorem EuclidGeom.Line.mkPtProj_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (dir : EuclidGeom.Dir) : EuclidGeom.Line.mk_pt_proj A dir.toProj = EuclidGeom.Line.mk_pt_dir A dir

def EuclidGeom.Line.mk_pt_vec_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (vec_nd : EuclidGeom.VecND) : EuclidGeom.Line P

Given a point $A$ and a nondegenerate vector, this function returns the line through $A$ along the nondegenerate vector.

Equations

• EuclidGeom.Line.mk_pt_vec_nd A vec_nd = EuclidGeom.Line.mk_pt_proj A vec_nd.toProj

def EuclidGeom.termLIN______ : Lean.ParserDescr

Given two distinct points $A$ and $B$, this function returns the line passing through $A$ and $B$. We use $\verb|LIN| A B$ or $\verb|LIN| A B h$ to abbreviate $\verb|Line.mk_pt_pt| A B h$, where $h$ is a statement that $A \neq B$. When such statement $h$ is missing, we search it in all the known facts.

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.delabLineMkPtPt : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for Line.mk_pt_pt

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.termDLIN______ : Lean.ParserDescr

Given two distinct points $A$ and $B$, this function returns the directed line starting from $A$ in the direction of $B$. We use $\verb|DLIN| A B$ or $\verb|DLIN| A B h$ to abbreviate $\verb|DLine.mk_pt_pt| A B h$, where $h$ is a statement that $A \neq B$. When such statement $h$ is missing, we search it in all the known facts.

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.delabDirLineMkPtPt : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for DirLine.mk_pt_pt

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.DirLine.toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) : EuclidGeom.Dir

Given a directed line, this function returns its direction.

Equations

• l.toDir = Quotient.lift (fun (ray : EuclidGeom.Ray P) => ray.toDir) (_ : ∀ (x x_1 : EuclidGeom.Ray P), x ≈ x_1 → x.toDir = x_1.toDir) l

@[inline, reducible]

abbrev EuclidGeom.DirLine.toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) : EuclidGeom.Proj

Given a directed line, this function returns its projected direction.

Equations

• l.toProj = l.toDir.toProj

def EuclidGeom.DirLine.toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) : EuclidGeom.Line P

Given a directed line, this function returns the associated line.

Equations

• l.toLine = Quotient.lift (fun (x : EuclidGeom.Ray P) => ⟦x⟧) (_ : ∀ (x x_1 : EuclidGeom.Ray P), x ≈ x_1 → ⟦x⟧ = ⟦x_1⟧) l

@[inline, reducible]

abbrev EuclidGeom.Ray.toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray : EuclidGeom.Ray P) : EuclidGeom.DirLine P

Given a ray, this function returns the associated directed line.

Equations

• ray.toDirLine = ⟦ray⟧

@[inline, reducible]

abbrev EuclidGeom.SegND.toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg_nd : EuclidGeom.SegND P) : EuclidGeom.DirLine P

Given a nondegenerate segment, this function returns the directed line in the direction of the segment.

Equations

• seg_nd.toDirLine = seg_nd.toDirLine

def EuclidGeom.Line.toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Line P) : EuclidGeom.Proj

Given a line, this function returns its projective direction.

Equations

• l.toProj = Quotient.lift (fun (ray : EuclidGeom.Ray P) => ray.toProj) (_ : ∀ (x x_1 : EuclidGeom.Ray P), x ≈ x_1 → x.toProj = x_1.toProj) l

@[inline, reducible]

abbrev EuclidGeom.Ray.toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray : EuclidGeom.Ray P) : EuclidGeom.Line P

Given a ray, this function returns the line associated with the ray.

Equations

• ray.toLine = ⟦ray⟧

@[inline, reducible]

abbrev EuclidGeom.SegND.toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg_nd : EuclidGeom.SegND P) : EuclidGeom.Line P

Given a nondegenerate segment, this function returns the line associated with the ray.

Equations

• seg_nd.toLine = ⟦seg_nd.toRay⟧

theorem EuclidGeom.DirLine.ind {P : Type u_1} [EuclidGeom.EuclideanPlane P] {C : EuclidGeom.DirLine P → Prop} (h : ∀ (r : EuclidGeom.Ray P), C r.toDirLine) (l : EuclidGeom.DirLine P) : C l

An induction principle to deduce results for directed lines from those for rays, used with induction l using DirLine.ind or induction' l using DirLine.ind with r.

theorem EuclidGeom.Line.ind {P : Type u_1} [EuclidGeom.EuclideanPlane P] {C : EuclidGeom.Line P → Prop} (h : ∀ (r : EuclidGeom.Ray P), C r.toLine) (l : EuclidGeom.Line P) : C l

An induction principle to deduce results for lines from those for rays, used with induction l using Line.ind or induction' l using Line.ind with r.

@[simp]

theorem EuclidGeom.mkPtProj_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (dir : EuclidGeom.Dir) : { source := A, toDir := dir }.toLine = EuclidGeom.Line.mk_pt_dir A dir

Given a point $A$ and a direction $dir$, the line associated to the ray starting at $A$ in the direction of $dir$ is the same as the line through $A$ in the direction of $dir$.

theorem EuclidGeom.DirLine.toLine_toProj_eq_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) : l.toLine.toProj = l.toProj

Given a directed line $l$, its projective direction is the same as the projective direction of the line associated to $l$.

theorem EuclidGeom.Ray.toLine_eq_toDirLine_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray : EuclidGeom.Ray P) : ray.toLine = ray.toDirLine.toLine

The line associated to a ray is the same as the line associated to the directed line of the ray.

instance EuclidGeom.instCoeRayDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] : Coe (EuclidGeom.Ray P) (EuclidGeom.DirLine P)

For coercion purpose, a ray can induce a directed line.

Equations

• EuclidGeom.instCoeRayDirLine = { coe := EuclidGeom.Ray.toDirLine }

instance EuclidGeom.instCoeDirLineLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] : Coe (EuclidGeom.DirLine P) (EuclidGeom.Line P)

For coercion purpose, a directed line can induce a line.

Equations

• EuclidGeom.instCoeDirLineLine = { coe := EuclidGeom.DirLine.toLine }

instance EuclidGeom.instCoeRayLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] : Coe (EuclidGeom.Ray P) (EuclidGeom.Line P)

For coercion purpose, a ray can induce a line.

Equations

• EuclidGeom.instCoeRayLine = { coe := EuclidGeom.Ray.toLine }

def EuclidGeom.Line.carrier {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Line P) : Set P

Given a line $l$, this function returns the set of points that lies on the line $l$.

Equations

• One or more equations did not get rendered due to their size.

def EuclidGeom.Line.IsOn {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.Line P) : Prop

This function returns whether a point $A$ lies on a line $l$ or not. Note that no definition of LiesInt is given.

Equations

• EuclidGeom.Line.IsOn A l = (A ∈ EuclidGeom.Line.carrier l)

instance EuclidGeom.Line.instFigLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.Fig (EuclidGeom.Line P) P

A line is a figure in the Euclidean geometry, meaning that one can talk about its underlying subset of points.

Equations

• EuclidGeom.Line.instFigLine = { carrier := EuclidGeom.Line.carrier }

@[inline, reducible]

abbrev EuclidGeom.DirLine.carrier {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) : Set P

For a directed line, this function returns its underlying subset.

Equations

• EuclidGeom.DirLine.carrier l = EuclidGeom.Line.carrier l.toLine

instance EuclidGeom.DirLine.instFigDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.Fig (EuclidGeom.DirLine P) P

A directed line is a figure in the Euclidean geometry, meaning that one can talk about its underlying subset of points.

Equations

• EuclidGeom.DirLine.instFigDirLine = { carrier := EuclidGeom.DirLine.carrier }

theorem EuclidGeom.Ray.toLine_carrier_eq_ray_carrier_union_rev_carrier {P : Type u_1} [EuclidGeom.EuclideanPlane P] (r : EuclidGeom.Ray P) : EuclidGeom.Line.carrier r.toLine = EuclidGeom.Ray.carrier r ∪ EuclidGeom.Ray.carrier r.reverse

The underlying set of the line associated to a ray is teh union of the underlying set of the ray and the underlying set of the reverse of the ray.

theorem EuclidGeom.Ray.lies_on_toLine_iff_lies_on_or_lies_on_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {r : EuclidGeom.Ray P} : EuclidGeom.lies_on A r.toLine ↔ EuclidGeom.lies_on A r ∨ EuclidGeom.lies_on A r.reverse

A point lies on a line associated to a ray if and only if it lies on the ray or the reverse of the ray.

theorem EuclidGeom.Ray.lies_on_toDirLine_iff_lies_on_or_lies_on_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {r : EuclidGeom.Ray P} : EuclidGeom.lies_on A r.toDirLine ↔ EuclidGeom.lies_on A r ∨ EuclidGeom.lies_on A r.reverse

This theorem states that a point A lies on the directed line associated to a ray r if and only if A lies on the ray r or A lies on the reverse of the ray r.

theorem EuclidGeom.DirLine.lies_on_iff_lies_on_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l : EuclidGeom.DirLine P} : EuclidGeom.lies_on A l.toLine ↔ EuclidGeom.lies_on A l

A point lies on the line associated to a directed line if and only if it lies on the line.

theorem EuclidGeom.Ray.lies_on_toLine_of_lie_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {r : EuclidGeom.Ray P} (h : EuclidGeom.lies_on A r) : EuclidGeom.lies_on A r.toLine

If a point lies on a ray, then it lies on the line associated to the ray.

theorem EuclidGeom.SegND.lies_on_toLine_of_lie_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_on A ↑s) : EuclidGeom.lies_on A s.toLine

Given a point A lying on a nondegenerate segment s, the point A also lies on the line associated to s.

theorem EuclidGeom.Ray.source_lies_on_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} : EuclidGeom.lies_on r.source r.toLine

The source of a ray lies on the line associated to the ray.

theorem EuclidGeom.SegND.source_lies_on_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : EuclidGeom.lies_on (↑s).source s.toLine

The source of a nondegenerate segment lies on the line associated to the segment.

theorem EuclidGeom.SegND.target_lies_on_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : EuclidGeom.lies_on (↑s).target s.toLine

The target point of a nondegenerate segment lies on the line associated to the segment.

theorem EuclidGeom.Ray.lies_on_toDirLine_of_lie_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {r : EuclidGeom.Ray P} (h : EuclidGeom.lies_on A r) : EuclidGeom.lies_on A r.toDirLine

If a point lies on a ray, then it lies on the directed line associated to the ray.

theorem EuclidGeom.SegND.lies_on_toDirLine_of_lie_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_on A ↑s) : EuclidGeom.lies_on A s.toDirLine

This theorem states that if a point A lies on a nondegenerate segment s, then A also lies on the directed line associated to s.

theorem EuclidGeom.Ray.source_lies_on_toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} : EuclidGeom.lies_on r.source r.toDirLine

The source of a ray lies on the directed line associated to the ray.

theorem EuclidGeom.SegND.source_lies_on_toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : EuclidGeom.lies_on (↑s).source s.toDirLine

The source of a nondegenerate segment lies on the directed line associated to the segment.

theorem EuclidGeom.SegND.target_lies_on_toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : EuclidGeom.lies_on (↑s).target s.toDirLine

The target point of a nondegenerate segment lies on the directed line associated to the segment.

def EuclidGeom.Ray.mk_pt_dirline {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.DirLine P) (_h : EuclidGeom.lies_on A l) : EuclidGeom.Ray P

Given a point $A$ lying on a directed line $l$, this function returns the ray starting from $A$ in the direction of $l$.

Equations

• EuclidGeom.Ray.mk_pt_dirline A l _h = { source := A, toDir := l.toDir }

theorem EuclidGeom.ray_of_pt_dirline_toDirLine_eq_dirline {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (l : EuclidGeom.DirLine P) (h : EuclidGeom.lies_on A l) : (EuclidGeom.Ray.mk_pt_dirline A l h).toDirLine = l

Given a point $A$ lying on a directed line $l$, the directed line associated to the ray from $A$ in the direction of $l$ is precisely $l$ itself.

theorem EuclidGeom.ray_of_pt_dirline_toDirLine_toDir_eq_dirline_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l : EuclidGeom.DirLine P} (h : EuclidGeom.lies_on A l) : (EuclidGeom.Ray.mk_pt_dirline A l h).toDir = l.toDir

Given a point A lying on a directed line l, the direction of the ray starting from A in the direction of l is the same as the direction of l.

def EuclidGeom.DirLine.reverse {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) : EuclidGeom.DirLine P

Given a directed line, the function returns the reverse of the directed line.

Equations

• l.reverse = Quotient.lift (fun (x : EuclidGeom.Ray P) => ⟦x.reverse⟧) (_ : ∀ (a b : EuclidGeom.Ray P), a ≈ b → ⟦a.reverse⟧ = ⟦b.reverse⟧) l

theorem EuclidGeom.DirLine.rev_toDir_eq_neg_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} : l.reverse.toDir = -l.toDir

Given a directed line $l$, the direction of its reverse is the opposite of its direction.

theorem EuclidGeom.DirLine.rev_rev_eq_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} : l.reverse.reverse = l

The reverse of the reverse of a directed line is the line itself.

theorem EuclidGeom.DirLine.lies_on_rev_iff_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l : EuclidGeom.DirLine P} : EuclidGeom.lies_on A l.reverse ↔ EuclidGeom.lies_on A l

A point lies on the reverse of a directed line if and only if it lies on the directed line.

theorem EuclidGeom.DirLine.rev_toLine_eq_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) : l.reverse.toLine = l.toLine

Given a directed line $l$, the line associted to the reverse of $l$ is the same as the line associated to $l$.

theorem EuclidGeom.DirLine.eq_of_toDir_eq_of_toLine_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l₁ : EuclidGeom.DirLine P} {l₂ : EuclidGeom.DirLine P} (h : l₁.toLine = l₂.toLine) (hd : l₁.toDir = l₂.toDir) : l₁ = l₂

Given two directed lines $l_1$ and $l_2$ with the same associated line, if they have the same direcdtion, they are equal.

theorem EuclidGeom.DirLine.eq_rev_of_toDir_eq_neg_of_toLine_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l₁ : EuclidGeom.DirLine P} {l₂ : EuclidGeom.DirLine P} (h : l₁.toLine = l₂.toLine) (hd : l₁.toDir = -l₂.toDir) : l₁ = l₂.reverse

Given two directed lines $l_1$ and $l_2$ with the same associated line, if they have the opposite direction, they are reverse of each other.

theorem EuclidGeom.DirLine.eq_rev_of_toDir_ne_of_toLine_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l₁ : EuclidGeom.DirLine P} {l₂ : EuclidGeom.DirLine P} (h : l₁.toLine = l₂.toLine) (hd : l₁.toDir ≠ l₂.toDir) : l₁ = l₂.reverse

Given two directed lines $l_1$ and $l_2$ with the same associated line, if they have different directions, then $l_1$ is the reverse of $l_2$.

theorem EuclidGeom.DirLine.eq_or_eq_rev_of_toLine_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l₁ : EuclidGeom.DirLine P} {l₂ : EuclidGeom.DirLine P} (h : l₁.toLine = l₂.toLine) : l₁ = l₂ ∨ l₁ = l₂.reverse

Given two directed lines $l_1$ and $l_2$, if their associated lines are equal, then either the directed lines are equal or one is the reverse of the other.

theorem EuclidGeom.Line.line_of_pt_pt_eq_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : LIN A B = LIN B A

Let $A$ and $B$ be two distinct points, the line through $A$ and $B$ is the same as the line through $B$ and $A$.

theorem EuclidGeom.Line.fst_pt_lies_on_mk_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : EuclidGeom.lies_on A (LIN A B)

For two distinct points $A$ and $B$, $A$ lies on the line through $A$ and $B$.

theorem EuclidGeom.Line.snd_pt_lies_on_mk_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : EuclidGeom.lies_on B (LIN A B)

The point $B$ lies on the line through $A$ and $B$.

theorem EuclidGeom.Line.pt_lies_on_line_of_pt_pt_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : EuclidGeom.lies_on A (LIN A B) ∧ EuclidGeom.lies_on B (LIN A B)

The first point and the second point in Line.mk_pt_pt LiesOn the line it makes.

theorem EuclidGeom.Line.eq_line_of_pt_pt_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} [_h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : LIN A B = l

Two point determines a line, i.e. given two distinct points $A$ and $B$ on a line $l$, the line through $A$ and $B$ is the same as $l$.

theorem EuclidGeom.Line.eq_of_pt_pt_lies_on_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] {l₁ : EuclidGeom.Line P} {l₂ : EuclidGeom.Line P} (hA₁ : EuclidGeom.lies_on A l₁) (hB₁ : EuclidGeom.lies_on B l₁) (hA₂ : EuclidGeom.lies_on A l₂) (hB₂ : EuclidGeom.lies_on B l₂) : l₁ = l₂

If two lines have two distinct intersection points, then these two lines are identical.

theorem EuclidGeom.Line.eq_pt_pt_line_iff_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} [_h : EuclidGeom.PtNe B A] : EuclidGeom.lies_on A l ∧ EuclidGeom.lies_on B l ↔ LIN A B = l

The theorem states that two distinct points A and B lie on a line $l$ if and only if the line through $A$ and $B$ is equal to $l$.

theorem EuclidGeom.Line.pt_pt_lies_on_iff_ray_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} [_h : EuclidGeom.PtNe B A] : EuclidGeom.lies_on A l ∧ EuclidGeom.lies_on B l ↔ (RAY A B).toLine = l

The theorem states that two distinct points $A$ and $B$ lie on a line $l$ if and only if the line associated to the ray from $A$ to $B$ is equal to $l$.

theorem EuclidGeom.Line.pt_pt_lies_on_iff_seg_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} [_h : EuclidGeom.PtNe B A] : EuclidGeom.lies_on A l ∧ EuclidGeom.lies_on B l ↔ (SEG_nd A B).toLine = l

The theorem states that two distinct points $A$ and $B$ lies on a line $l$ if and only if the line associated with the nondegenerate segment $AB$ is the same as line $l$.

theorem EuclidGeom.Line.toProj_eq_seg_nd_toProj_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) [_hab : EuclidGeom.PtNe B A] : (SEG_nd A B).toProj = l.toProj

Given two distinct points $A$ and $B$ lying on a line $l$, the projective direction of the nondegenerate segment $AB$ is the same as the projective direction of the line $l$.

theorem EuclidGeom.Line.pt_lies_on_of_mk_pt_proj {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (proj : EuclidGeom.Proj) : EuclidGeom.lies_on A (EuclidGeom.Line.mk_pt_proj A proj)

Given a point $A$ and a projective direction, $A$ lies on the line through $A$ in the direction of the projective direction.

theorem EuclidGeom.Line.pt_lies_on_of_mk_pt_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (dir : EuclidGeom.Dir) : EuclidGeom.lies_on A (EuclidGeom.Line.mk_pt_dir A dir)

Given a point $A$ and a direction, $A$ lies on the line through $A$ along the given direction.

theorem EuclidGeom.Line.pt_lies_on_of_mk_pt_vec_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (vec_nd : EuclidGeom.VecND) : EuclidGeom.lies_on A (EuclidGeom.Line.mk_pt_vec_nd A vec_nd)

Given a point $A$ and a nondegenerate vector, then $A$ lies on the line through $A$ in the direction of the given vector.

theorem EuclidGeom.Line.proj_eq_of_mk_pt_proj {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (proj : EuclidGeom.Proj) : (EuclidGeom.Line.mk_pt_proj A proj).toProj = proj

Given a point $A$ and a projective direction $proj$, the projective direction of the line through $A$ and in the projective direction $proj$ is exactly $proj$.

theorem EuclidGeom.Line.mk_pt_proj_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l : EuclidGeom.Line P} (h : EuclidGeom.lies_on A l) : EuclidGeom.Line.mk_pt_proj A l.toProj = l

Given a point $A$ lying on a line $l$, the line through $A$ along the projective direction of $l$ is precisely $l$.

theorem EuclidGeom.Line.mk_pt_proj_eq_of_eq_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l : EuclidGeom.Line P} (h : EuclidGeom.lies_on A l) {x : EuclidGeom.Proj} (hx : x = l.toProj) : EuclidGeom.Line.mk_pt_proj A x = l

Given a projective direction $x$ and a point $A$ on a line $l$, if $x$ is the same as the projective direction of $l$, then the line through $A$ in the direction of $x$ is equal to $l$.

theorem EuclidGeom.Line.eq_of_same_toProj_and_pt_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l₁ : EuclidGeom.Line P} {l₂ : EuclidGeom.Line P} (h₁ : EuclidGeom.lies_on A l₁) (h₂ : EuclidGeom.lies_on A l₂) (h : l₁.toProj = l₂.toProj) : l₁ = l₂

Given two lines $l_1$ and $l_2$ with the same projective direction, if there is a point $A$ that lies on both lines, then $l_1 = l_2$.

theorem EuclidGeom.Line.exist_rep_ray_source_eq_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.Line P} {A : P} (ha : EuclidGeom.lies_on A l) : ∃ (r : EuclidGeom.Ray P), r.source = A ∧ r.toLine = l

theorem EuclidGeom.exist_line_pt_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) : ∃ (l : EuclidGeom.Line P), EuclidGeom.lies_on A l

Given a point $A$, there exists a line through $A$.

theorem EuclidGeom.exist_line_of_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) : ∃ (l : EuclidGeom.Line P), EuclidGeom.lies_on A l ∧ EuclidGeom.lies_on B l

theorem EuclidGeom.DirLine.pt_pt_rev_eq_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : DLIN B A = (DLIN A B).reverse

Given two distinct points, the directed line from $B$ to $A$ is the reverse of the directed line from $A$ to $B$.

theorem EuclidGeom.DirLine.fst_pt_lies_on_mk_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : EuclidGeom.lies_on A (DLIN A B)

For two distinct points $A$ and $B$, $A$ lies on the directed line from $A$ to $B$.

theorem EuclidGeom.DirLine.snd_pt_lies_on_mk_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : EuclidGeom.lies_on B (DLIN A B)

For two distinct points $A$ and $B$, the second point $B$ lies on the directed line from $A$ to $B$.

theorem EuclidGeom.DirLine.pt_lies_on_of_pt_pt_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : EuclidGeom.lies_on A (DLIN A B) ∧ EuclidGeom.lies_on B (DLIN A B)

Given two distinct points $A$ and $B$, both $A$ and $B$ lie on the directed line from $A$ to $B$.

theorem EuclidGeom.DirLine.pt_lies_on_of_mk_pt_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (dir : EuclidGeom.Dir) : EuclidGeom.lies_on A (EuclidGeom.DirLine.mk_pt_dir A dir)

Given a point $A$ and a direction, the point $A$ lies on the line through $A$ in the given direction.

theorem EuclidGeom.DirLine.pt_lies_on_of_mk_pt_vec_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (vec_nd : EuclidGeom.VecND) : EuclidGeom.lies_on A (EuclidGeom.DirLine.mk_pt_vec_nd A vec_nd)

Given a point and a nondegenerate vector, $A$ lies on the directed line from $A$ in the direction of the given vector.

theorem EuclidGeom.DirLine.dir_eq_of_mk_pt_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (dir : EuclidGeom.Dir) : (EuclidGeom.DirLine.mk_pt_dir A dir).toDir = dir

The direction of the directed line from a point $A$ in the direction of $dir$ is $dir$ itself.

theorem EuclidGeom.DirLine.mk_pt_dir_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l : EuclidGeom.DirLine P} (h : EuclidGeom.lies_on A l) : EuclidGeom.DirLine.mk_pt_dir A l.toDir = l

Given a point $A$ lying on a directed line $l$, this theorem states that the directed line from $A$ in the direction of $l$ is the same as $l$ itself.

theorem EuclidGeom.DirLine.mk_pt_dir_eq_of_eq_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l : EuclidGeom.DirLine P} (h : EuclidGeom.lies_on A l) {x : EuclidGeom.Dir} (hx : x = l.toDir) : EuclidGeom.DirLine.mk_pt_dir A x = l

Given a point $A$ and a directed line $l$, if $A$ lies on $l$, then the directed line from $A$ in the direction of $l$ is the same as $l$.

theorem EuclidGeom.DirLine.eq_of_same_toDir_and_pt_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {l₁ : EuclidGeom.DirLine P} {l₂ : EuclidGeom.DirLine P} (h₁ : EuclidGeom.lies_on A l₁) (h₂ : EuclidGeom.lies_on A l₂) (h : l₁.toDir = l₂.toDir) : l₁ = l₂

If two directed lines have a intersection point and the same direction, then these two directed lines are identical.

theorem EuclidGeom.DirLine.eq_dirline_of_toDir_eq_of_pt_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} [_h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A l) (hd : (SEG_nd A B).toDir = l.toDir) : DLIN A B = l

Given two distinct points $A$ and $B$, if $A$ lies on $l$ and the direction of the nondegenerate segment $AB$ is the same as the direction of a directed line $l$, then the directed line from $A$ to $B$ is the same as $l$.

theorem EuclidGeom.DirLine.eq_dirline_rev_of_toDir_ne_of_pt_pt_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} [_h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) (hd : (SEG_nd A B).toDir ≠ l.toDir) : DLIN B A = l

Given two distinct points $A$ and $B$ on a directed line $l$, if the direction of the nondegenerate segment $AB$ is not the same as the direction of $l$, then the directed line from $B$ to $A$ is $l$.

theorem EuclidGeom.DirLine.eq_dirline_or_rev_of_pt_pt_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} [_h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : DLIN A B = l ∨ DLIN B A = l

If $A$ and $B$ are two distinct points that both lie on the same directed line $l$, then $l$ is either the directed line from $A$ to $B$ or the directed line from $B$ to $A$.

theorem EuclidGeom.DirLine.eq_dirline_or_rev_of_pt_pt_lies_on_of_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] {l₁ : EuclidGeom.DirLine P} {l₂ : EuclidGeom.DirLine P} (hA₁ : EuclidGeom.lies_on A l₁) (hB₁ : EuclidGeom.lies_on B l₁) (hA₂ : EuclidGeom.lies_on A l₂) (hB₂ : EuclidGeom.lies_on B l₂) : l₁ = l₂ ∨ l₁ = l₂.reverse

Given two distinct points $A$ and $B$ and two directed line $l_1$ and $l_2$, assume that both $A$ and $B$ lie on $l_1$ and both $A$ and $B$ lie on $l_2$, then either $l_1$ is equal to $l_2$ or $l_1$ is equal to the reverse of $l_2$.

theorem EuclidGeom.DirLine.toProj_eq_seg_nd_toProj_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) [_h : EuclidGeom.PtNe B A] : (SEG_nd A B).toProj = l.toProj

If $A$ and $B$ are two distinct points that both lie on a directed line $l$, then the projective direction of the nondegenerate segment $AB$ is the same as the projective direction of $l$.

theorem EuclidGeom.exist_dirline_pt_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) : ∃ (l : EuclidGeom.DirLine P), EuclidGeom.lies_on A l

Given a point $A$, there exists a directed line $l$ such that $A$ lies on $l$.

theorem EuclidGeom.Ray.toLine_eq_rev_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} : r.toLine = r.reverse.toLine

The line associated with a ray is the same as the line associated with its reverse.

theorem EuclidGeom.SegND.toLine_eq_toRay_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : s.toLine = s.toLine

The line associated to a nondegenerate segment is the same as the line associated to its extension ray.

theorem EuclidGeom.SegND.toLine_eq_rev_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : s.toLine = (EuclidGeom.SegND.reverse s).toLine

The line associated to a nondegenerate segment is the same as the line associated to its reverse.

theorem EuclidGeom.SegND.toLine_eq_extn_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : s.toLine = (EuclidGeom.SegND.extension s).toLine

For a nondegenerate segment $s$, the line associated to $s$ is the same as the line associated to the ray of $s$.

theorem EuclidGeom.ray_of_pt_pt_toLine_eq_line_of_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : (RAY A B).toLine = LIN A B

For two distinct points $A$ and $B$, the line associated to the ray from $A$ to $B$ is the same as the line through $A$ and $B$.

theorem EuclidGeom.seg_nd_of_pt_pt_toLine_eq_line_of_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : (SEG_nd A B).toLine = LIN A B

The line associated to the nondegenerate segment $AB$ is the same as the line through $A$ and $B$.

theorem EuclidGeom.Ray.toDirLine_rev_eq_rev_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} : r.toDirLine.reverse = r.reverse.toDirLine

The reverse of the directed line associated to a ray is the directed line associated to the reverse of the ray.

theorem EuclidGeom.SegND.toDirLine_eq_toRay_toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : s.toDirLine = s.toDirLine

The directed line associated with a nondegenerate segment is the same as the directed line associated with the ray of the segment.

theorem EuclidGeom.SegND.toDirLine_rev_eq_rev_toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : s.toDirLine.reverse = (EuclidGeom.SegND.reverse s).toDirLine

The reverse of the directed line associated to a nondegenerate segment is the directed line associated to the reverse of the segment.

theorem EuclidGeom.SegND.toDirLine_eq_extn_toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : s.toDirLine = (EuclidGeom.SegND.extension s).toDirLine

The directed line associated with a nondegenerate segment is the same as the directed line associated with its extension.

theorem EuclidGeom.ray_of_pt_pt_toDirLine_eq_dirline_of_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : (RAY A B).toDirLine = DLIN A B

Let $A$ and $B$ be two distinct points, then the directed line from $A$ to $B$ is the same as the directed line associated to the ray $\overrightarrow{AB}$.

theorem EuclidGeom.seg_nd_of_pt_pt_toDirLine_eq_dirline_of_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : (SEG_nd A B).toDirLine = DLIN A B

Given two distinct points $A$ and $B$, the directed line from $A$ to $B$ is the same as the directed line associated to the nondegenerate segment $AB$.

theorem EuclidGeom.Ray.subset_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} : EuclidGeom.Ray.carrier r ⊆ EuclidGeom.Line.carrier r.toLine

The underlying set of a ray is a subset of the underlying set of the line associated to the ray.

theorem EuclidGeom.ray_subset_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {l : EuclidGeom.Line P} (h : r.toLine = l) : EuclidGeom.Ray.carrier r ⊆ EuclidGeom.Line.carrier l

The underlying set of a ray is a subset of the underlying set of the line associated to the ray.

theorem EuclidGeom.SegND.lies_on_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} {A : P} (h : EuclidGeom.lies_on A s) : EuclidGeom.lies_on A s.toLine

Given a point $A$ lying on a nondegenerate segment $s$, the point $A$ also lies on the line associated to $s$.

theorem EuclidGeom.SegND.subset_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : EuclidGeom.SegND.carrier s ⊆ EuclidGeom.Line.carrier s.toLine

The underlying set of a nondegenerate segment $s$ is a subset of the underlying set of the line associated to $s$.

theorem EuclidGeom.seg_subset_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} {l : EuclidGeom.Line P} (h : s.toLine = l) : EuclidGeom.SegND.carrier s ⊆ EuclidGeom.Line.carrier l

The underlying set of a nondegenerate segment is a subset of the underlying set of the line associated to the segment.

theorem EuclidGeom.Line.nontriv {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Line P) : ∃ (A : P) (B : P), EuclidGeom.lies_on A l ∧ EuclidGeom.lies_on B l ∧ B ≠ A

The theorem states that for any line $l$, there exist two distinct points $A$ and $B$ such that $A$ and $B$ both lie on the line $l$.

theorem EuclidGeom.Ray.lies_on_toLine_iff_lies_int_or_lies_int_rev_or_eq_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {r : EuclidGeom.Ray P} : EuclidGeom.lies_on A r.toLine ↔ EuclidGeom.lies_int A r ∨ EuclidGeom.lies_int A r.reverse ∨ A = r.source

Given a point and a ray $r$, $A$ lies on the line associated to $r$ if and only if $A$ lies either in the interior of $r$ or the interior of the reverse of $r$ or $A$ is the source of $r$.

theorem EuclidGeom.SegND.lies_on_extn_or_rev_extn_iff_lies_on_toLine_of_not_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (h : ¬EuclidGeom.lies_int A ↑seg_nd) : EuclidGeom.lies_on A seg_nd.toLine ↔ EuclidGeom.lies_on A (EuclidGeom.SegND.extension seg_nd) ∨ EuclidGeom.lies_on A (EuclidGeom.SegND.extension (EuclidGeom.SegND.reverse seg_nd))

If a point $A$ does not lie in the interior of a nondegenerate segment, then $A$ lies on the line of the segment if and only if it lies on the extension ray of the segment or it lies on the extension ray of the reverse of the segment.

theorem EuclidGeom.SegND.lies_on_toLine_of_lies_on_extn {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} (lieson : EuclidGeom.lies_on X (EuclidGeom.SegND.extension seg_nd)) : EuclidGeom.lies_on X seg_nd.toLine

Given a point $X$ and a nondegenerate segment $seg_nd$, if $X$ lies on the extension ray of $seg_nd$, then $X$ lies on the line associated with $seg_nd$.

theorem EuclidGeom.lies_on_iff_lies_on_iff_line_eq_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l₁ : EuclidGeom.Line P) (l₂ : EuclidGeom.Line P) : (∀ (A : P), EuclidGeom.lies_on A l₁ ↔ EuclidGeom.lies_on A l₂) ↔ l₁ = l₂

Two lines are equal iff they have the same underlying sets.

theorem EuclidGeom.Line.lies_on_iff_eq_toProj_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} [_h : EuclidGeom.PtNe B A] (hA : EuclidGeom.lies_on A l) : EuclidGeom.lies_on B l ↔ (SEG_nd A B).toProj = l.toProj

If $A$ and $B$ are two distinct points and $A$ lies on a line $l$, the point $B$ lies on the line $l$ if and only if the projective direction of the nondegenerate segment $AB$ is the same as the projective direction of $l$.

theorem EuclidGeom.Line.exist_real_vec_eq_smul_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {dir : EuclidGeom.Dir} (h : EuclidGeom.lies_on B (EuclidGeom.Line.mk_pt_dir A dir)) : ∃ (t : ℝ), EuclidGeom.Vec.mkPtPt A B = t • dir.unitVec

Let $A$ be a point and $B$ a point that lies on the line through $A$ in a given direction $dir$. Then there exists a real number $t$ such that the vector $\xrightarrow{AB}$ is $t$ times the unit vector of the direction $dir$.

theorem EuclidGeom.Line.exist_real_vec_eq_smul_vec_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {v : EuclidGeom.VecND} (hb : EuclidGeom.lies_on B (EuclidGeom.Line.mk_pt_vec_nd A v)) : ∃ (t : ℝ), EuclidGeom.Vec.mkPtPt A B = t • ↑v

If $A$ is a point and $v$ a nondegenerate vector and if a point $B$ lies on the line through $A$ in the direction of $v$, then there exists a real number $t$ such that the vector $AB$ is $t$ times the vector $v$, i.e. $\overrightarrow{AB} = t \cdot v$.

theorem EuclidGeom.Line.exist_real_of_lies_on_of_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [_h : EuclidGeom.PtNe B A] (hc : EuclidGeom.lies_on C (LIN A B)) : ∃ (t : ℝ), EuclidGeom.Vec.mkPtPt A C = t • EuclidGeom.Vec.mkPtPt A B

Given a point $C$ lying on the line through distinct points $A$ and $B$, there exists a real number $t$ such that the vector $\overrightarrow{AC}$ is $t$ times the vector $\overrightarrow{AB}$.

theorem EuclidGeom.Line.lies_on_of_exist_real_vec_eq_smul {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {dir : EuclidGeom.Dir} {t : ℝ} (h : EuclidGeom.Vec.mkPtPt A B = t • dir.unitVec) : EuclidGeom.lies_on B (EuclidGeom.Line.mk_pt_dir A dir)

For two points $A$ and $B$ and a direction vector $dir$, there exists a real number $t$ such that the vector $\overrightarrow{AB}$ is t times $dir$, then $B$ lies on the directed line from $A$ in the direction of $dir$.

theorem EuclidGeom.Line.lies_on_of_exist_real_vec_eq_smul_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {v : EuclidGeom.VecND} {t : ℝ} (h : EuclidGeom.Vec.mkPtPt A B = t • ↑v) : EuclidGeom.lies_on B (EuclidGeom.Line.mk_pt_vec_nd A v)

For two points $A$ and $B$ and a nondegenerate vector $v$, there exists a real number $t$ such that the vector $\overrightarrow{AB}$ is t times $v$, then $B$ lies on the directed line from $A$ in the direction of $v$.

theorem EuclidGeom.Line.lies_on_of_exist_real_of_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [_h : EuclidGeom.PtNe B A] {t : ℝ} (ht : EuclidGeom.Vec.mkPtPt A C = t • EuclidGeom.Vec.mkPtPt A B) : EuclidGeom.lies_on C (LIN A B)

Given points $A$, $B$, and $C$ with $A \neq B$, if there exists a real number t such that the vector $\overrightarrow {AC}$ is $t$ times the vector $\overrightarrow {AB}$, then $C$ lies on the line through $A$ and $B$.

theorem EuclidGeom.Ray.subset_toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} : EuclidGeom.Ray.carrier r ⊆ EuclidGeom.DirLine.carrier r.toDirLine

The theorem states that the set of points on a ray is a subset of the set of points on the directed line associated with the ray.

theorem EuclidGeom.ray_subset_dirline {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {l : EuclidGeom.DirLine P} (h : r.toDirLine = l) : EuclidGeom.Ray.carrier r ⊆ EuclidGeom.DirLine.carrier l

If a line $l$ is the directed line associated to a ray $r$, then the underlying set of $r$ is the subset of the underlying set of $l$.

theorem EuclidGeom.seg_lies_on_dirline {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} {A : P} (h : EuclidGeom.lies_on A ↑s) : EuclidGeom.lies_on A s.toDirLine

A point $A$ lying on a nondegenerate segment $s$ also lies on the directed line associated to $s$.

theorem EuclidGeom.SegND.subset_toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : EuclidGeom.SegND.carrier s ⊆ EuclidGeom.DirLine.carrier s.toDirLine

The underlying set of a nondegenerate segment $s$ is a subset of the underlying set of the line associated to $s$.

theorem EuclidGeom.seg_subset_dirline {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} {l : EuclidGeom.DirLine P} (h : s.toDirLine = l) : EuclidGeom.SegND.carrier s ⊆ EuclidGeom.DirLine.carrier l

If a directed line $l$ is the directed line associated to a nondegenerate segment $s$, then the underlying set of $s$ is a subset of the underlying set of $l$.

theorem EuclidGeom.DirLine.nontriv {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) : ∃ (A : P) (B : P), EuclidGeom.lies_on A l ∧ EuclidGeom.lies_on B l ∧ B ≠ A

On any directed line $l$, there exist two distinct points $A$ and $B$ on $l$.

theorem EuclidGeom.Ray.lies_on_toDirLine_iff_lies_int_or_lies_int_rev_or_eq_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {r : EuclidGeom.Ray P} : EuclidGeom.lies_on A r.toDirLine ↔ EuclidGeom.lies_int A r ∨ EuclidGeom.lies_int A r.reverse ∨ A = r.source

A point lies on a directed line associated to a ray $r$ if and only if it lies in the interior of $r$ or the interior of the reverse ray or $r$, or it is the source of $r$.

theorem EuclidGeom.SegND.lies_on_extn_or_rev_extn_iff_lies_on_toDirLine_of_not_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (h : ¬EuclidGeom.lies_int A ↑seg_nd) : EuclidGeom.lies_on A seg_nd.toDirLine ↔ EuclidGeom.lies_on A (EuclidGeom.SegND.extension seg_nd) ∨ EuclidGeom.lies_on A (EuclidGeom.SegND.extension (EuclidGeom.SegND.reverse seg_nd))

If a point $A$ does not lie in hte interior of a nondegenerate segement $seg_nd$, then it lies on the line associaeted to $seg_nd$ if and only if it lies on the extension ray of $seg_nd$ or it lies on the extension ray of the reverse of $seg_nd$.

theorem EuclidGeom.SegND.lies_on_toDirLine_of_lies_on_extn {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} (h : EuclidGeom.lies_on X (EuclidGeom.SegND.extension seg_nd)) : EuclidGeom.lies_on X seg_nd.toDirLine

This theorem states that if a point $X$ lies on the extension ray of a nondegenerate segment seg_nd, then X also lies on the directed line associated to seg_nd.

theorem EuclidGeom.DirLine.lies_on_iff_lies_on_iff_toLine_eq_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l₁ : EuclidGeom.DirLine P) (l₂ : EuclidGeom.DirLine P) : (∀ (A : P), EuclidGeom.lies_on A l₁ ↔ EuclidGeom.lies_on A l₂) ↔ l₁.toLine = l₂.toLine

For two directed lines $l_1$ and $l_2$, they have the same associated line if and only if for any point $A$, it lies on $l_1$ if and only if it lies on $l_2$.

theorem EuclidGeom.DirLine.lies_on_iff_eq_toProj_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} [_h : EuclidGeom.PtNe B A] (hA : EuclidGeom.lies_on A l) : EuclidGeom.lies_on B l ↔ (SEG_nd A B).toProj = l.toProj

Given two distinct points $A$ and $B$ and a directed line $l$, assume that $A$ lies on $l$, then $B$ lies on $l$ if and only if the projective direction of $l$ is the same as the projective direction of the segment $AB$.

theorem EuclidGeom.DirLine.exist_real_vec_eq_smul_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {dir : EuclidGeom.Dir} (h : EuclidGeom.lies_on B (EuclidGeom.DirLine.mk_pt_dir A dir)) : ∃ (t : ℝ), EuclidGeom.Vec.mkPtPt A B = t • dir.unitVec

Given a point $A$ and a direcction $dir$, if $B$ is a point that lies on the directed line through $A$ in the direction of $dir$, there exists a real number $t$ such that the vector $\overrightarrow{AB}$ is $t$ times the unit vector of the direction $dir$.

theorem EuclidGeom.DirLine.exist_real_vec_eq_smul_vec_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {v : EuclidGeom.VecND} (h : EuclidGeom.lies_on B (EuclidGeom.DirLine.mk_pt_vec_nd A v)) : ∃ (t : ℝ), EuclidGeom.Vec.mkPtPt A B = t • ↑v

If a point $B$ lies on the directed line through $A$ in the direction of a nondegenerate vector $v$, then the vector $\overrightarrow{AB}$ is some real multiple of $v$.

theorem EuclidGeom.DirLine.exist_real_of_lies_on_of_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [_h : EuclidGeom.PtNe B A] (hc : EuclidGeom.lies_on C (DLIN A B)) : ∃ (t : ℝ), EuclidGeom.Vec.mkPtPt A C = t • EuclidGeom.Vec.mkPtPt A B

Let $A$ and $B$ be two distinct points and $C$ a point that lies on the directed line from $A$ to $B$. Then there exists some real number $t$ such that $\xrightarrow{AC}$ is $t$ times $\xrightarrow{AB}$.

theorem EuclidGeom.DirLine.exist_real_vec_eq_smul_toDir_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : ∃ (t : ℝ), EuclidGeom.Vec.mkPtPt A B = t • l.toDir.unitVec

Given two points $A$ and $B$ on a directed line $l$, there exists a real number $t$ such that the vector $\xrightarrow{AB}$ is $t$ times the unit direction vector of $l$.

theorem EuclidGeom.DirLine.lies_on_of_exist_real_vec_eq_smul {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {dir : EuclidGeom.Dir} {t : ℝ} (h : EuclidGeom.Vec.mkPtPt A B = t • dir.unitVec) : EuclidGeom.lies_on B (EuclidGeom.DirLine.mk_pt_dir A dir)

Given two points $A$ and $B$ and a direction $dir$, if there exists a real number $t$ such that the vector $\overrightarrow{AB}$ is $t$ times the unit vector of the direction dir, then $B$ lies on the directed line from $A$ in the direction of $dir$.

theorem EuclidGeom.DirLine.lies_on_of_exist_real_vec_eq_smul_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {v : EuclidGeom.VecND} {t : ℝ} (h : EuclidGeom.Vec.mkPtPt A B = t • ↑v) : EuclidGeom.lies_on B (EuclidGeom.DirLine.mk_pt_vec_nd A v)

If the vector from a point $A$ to a point $B$ is a scalar multiple of a nondegenerate vector $v$, then $B$ lies on the directed line through $A$ in the direction of $v$.

theorem EuclidGeom.DirLine.lies_on_of_exist_real_of_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [_h : EuclidGeom.PtNe B A] {t : ℝ} (ht : EuclidGeom.Vec.mkPtPt A C = t • EuclidGeom.Vec.mkPtPt A B) : EuclidGeom.lies_on C (DLIN A B)

Given points $A$, $B$, and $C$, if $B$ and $A$ are distinct, and the vector $\overrightarrow {AC}$ is a real multiple of the vector $\overrightarrow{AB}$, then $C$ lies on the directed line from $A$ to $B$.

theorem EuclidGeom.DirLine.lies_on_of_exist_real_vec_eq_smul_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) {t : ℝ} (ht : EuclidGeom.Vec.mkPtPt A B = t • l.toDir.unitVec) : EuclidGeom.lies_on B l

Given a point $A$ on a directed line $l$, if for some point $B$ the vector $\overrightarrow{AB}$ is a real multiple of the unit direct vector of $l$, then $B$ lies on $l$.

theorem EuclidGeom.Ray.eq_toDirLine_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {r : EuclidGeom.Ray P} (h : EuclidGeom.lies_int A r) : DLIN r.source A (_ : A ≠ r.source) = r.toDirLine

theorem EuclidGeom.Ray.eq_toLine_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {r : EuclidGeom.Ray P} (h : EuclidGeom.lies_int A r) : LIN r.source A (_ : A ≠ r.source) = r.toLine

theorem EuclidGeom.SegND.dirLine_source_pt_eq_toDirLine_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_int A s) : DLIN s.source A (_ : A ≠ (↑s).source) = s.toDirLine

theorem EuclidGeom.SegND.line_source_pt_eq_toLine_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_int A s) : LIN s.source A (_ : A ≠ (↑s).source) = s.toLine

theorem EuclidGeom.SegND.dirLine_pt_target_eq_toDirLine_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_int A s) : DLIN A s.target (_ : (↑s).target ≠ A) = s.toDirLine

theorem EuclidGeom.SegND.line_pt_target_eq_toLine_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_int A s) : LIN A s.target (_ : (↑s).target ≠ A) = s.toLine

theorem EuclidGeom.SegND.dirLine_source_midpt_eq_toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : DLIN s.source (EuclidGeom.SegND.midpoint s) (_ : EuclidGeom.SegND.midpoint s ≠ s.source) = s.toDirLine

theorem EuclidGeom.SegND.line_source_midpt_eq_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : LIN s.source (EuclidGeom.SegND.midpoint s) (_ : EuclidGeom.SegND.midpoint s ≠ s.source) = s.toLine

theorem EuclidGeom.SegND.dirLine_midpt_target_eq_toDirLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : DLIN (EuclidGeom.SegND.midpoint s) s.target (_ : s.target ≠ EuclidGeom.SegND.midpoint s) = s.toDirLine

theorem EuclidGeom.SegND.line_midpt_target_eq_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.SegND P} : LIN (EuclidGeom.SegND.midpoint s) s.target (_ : s.target ≠ EuclidGeom.SegND.midpoint s) = s.toLine

theorem EuclidGeom.eq_or_vec_eq_of_dist_eq_of_lies_on_line_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [hne : EuclidGeom.PtNe B A] (h : EuclidGeom.lies_on C (LIN A B)) (heq : dist A C = dist A B) : C = B ∨ EuclidGeom.Vec.mkPtPt A C = EuclidGeom.Vec.mkPtPt B A

theorem EuclidGeom.vec_eq_dist_eq_of_lies_on_line_pt_pt_of_ptNe {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [_hne₁ : EuclidGeom.PtNe B A] [_hne₂ : EuclidGeom.PtNe C B] (h : EuclidGeom.lies_on C (LIN A B)) (heq : dist A C = dist A B) : EuclidGeom.Vec.mkPtPt B A = EuclidGeom.Vec.mkPtPt A C

theorem EuclidGeom.SegND.dist_midpt_le_iff_lies_on_of_lies_on_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_on A s.toLine) : dist A (EuclidGeom.SegND.midpoint s) < dist s.source (EuclidGeom.SegND.midpoint s) ↔ EuclidGeom.lies_int A s

theorem EuclidGeom.SegND.dist_midpt_lt_iff_lies_int_of_lies_on_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_on A s.toLine) : dist A (EuclidGeom.SegND.midpoint s) < dist s.source (EuclidGeom.SegND.midpoint s) ↔ EuclidGeom.lies_int A s

theorem EuclidGeom.SegND.dist_midpt_eq_iff_eq_source_or_eq_target_of_lies_on_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_on A s.toLine) : dist A (EuclidGeom.SegND.midpoint s) = dist s.source (EuclidGeom.SegND.midpoint s) ↔ A = s.source ∨ A = s.target

theorem EuclidGeom.SegND.dist_midpt_gt_iff_not_lies_on_of_lies_on_toLine {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_on A s.toLine) : dist s.source (EuclidGeom.SegND.midpoint s) < dist A (EuclidGeom.SegND.midpoint s) ↔ ¬EuclidGeom.lies_on A s

theorem EuclidGeom.lies_int_seg_nd_iff_lies_on_ray_reverse {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [hne₁ : EuclidGeom.PtNe B C] [hne₂ : EuclidGeom.PtNe A B] (h : EuclidGeom.lies_on A (LIN B C)) : EuclidGeom.lies_int A { source := B, target := C } ↔ EuclidGeom.lies_on C (RAY A B).reverse

theorem EuclidGeom.not_lies_on_seg_nd_iff_lies_on_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [hne₁ : EuclidGeom.PtNe B C] [hne₂ : EuclidGeom.PtNe A B] (h : EuclidGeom.lies_on A (LIN B C)) : ¬EuclidGeom.lies_on A { source := B, target := C } ↔ EuclidGeom.lies_on C (RAY A B)

theorem EuclidGeom.Line.pt_pt_linear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [_h : EuclidGeom.PtNe B A] (hc : EuclidGeom.lies_on C (LIN A B)) : EuclidGeom.Collinear A B C

Given three points $A$, $B$ and $C$, if $A$ and $B$ are distinct and $C$ lies on the line $AB$, then $A$, $B$, and $C$ are collinear.

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

The theorem states that if three points $A$, $B$, and $C$ lie on the same line $l$, then they are collinear.

theorem EuclidGeom.Line.pt_pt_maximal {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [_h : EuclidGeom.PtNe B A] (Co : EuclidGeom.Collinear A B C) : EuclidGeom.lies_on C (LIN A B)

If $A$ and $B$ are two distinct points and $C$ is a point such that $A$, $B$ and $C$ are collinear, then $C$ lies on the line $AB$.

theorem EuclidGeom.Line.maximal {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.Line P} {A : P} {B : P} {C : P} (h₁ : EuclidGeom.lies_on A l) (h₂ : EuclidGeom.lies_on B l) [_h : EuclidGeom.PtNe B A] (Co : EuclidGeom.Collinear A B C) : EuclidGeom.lies_on C l

Given two distinct points $A$ and $B$ on a line $l$, if a point $C$ is so that $A$, $B$, and $C$ are collinear, then $C$ lines on $l$.

theorem EuclidGeom.Line.lies_on_line_of_pt_pt_iff_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] (X : P) : EuclidGeom.lies_on X (LIN A B) ↔ EuclidGeom.Collinear A B X

Given two distinct points $A$ and $B$, a point $X$ lies on the line through $A$ and $B$ if and only if $A$, $B$, and $X$ are collinear.

theorem EuclidGeom.Line.lies_on_iff_collinear_of_ne_lies_on_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} [_h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) (C : P) : EuclidGeom.lies_on C l ↔ EuclidGeom.Collinear A B C

This theorem states that if $A$ and $B$ are two distinct points on a line $l$, then a point $C$ lies on $l$ if and only if $A$, $B$, and $C$ are collinear.

theorem EuclidGeom.Line.ne_pt_pt_of_not_collinear_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [_h : EuclidGeom.PtNe B A] {l : EuclidGeom.Line P} (hc : EuclidGeom.lies_on C l) (h : ¬EuclidGeom.Collinear A B C) : l ≠ LIN A B

theorem EuclidGeom.exist_line_lies_on_of_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} (h : EuclidGeom.Collinear A B C) : ∃ (l : EuclidGeom.Line P), EuclidGeom.lies_on A l ∧ EuclidGeom.lies_on B l ∧ EuclidGeom.lies_on C l

theorem EuclidGeom.collinear_iff_exist_line_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : EuclidGeom.Collinear A B C ↔ ∃ (l : EuclidGeom.Line P), EuclidGeom.lies_on A l ∧ EuclidGeom.lies_on B l ∧ EuclidGeom.lies_on C l

The given theorem is an equivalence statement between the collinearity of three points and the existence of a line on which all three points lie.

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

If $A$, $B$ and $C$ are three points on the same directed line $l$, then they are collinear.

theorem EuclidGeom.DirLine.pt_pt_maximal {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {C : P} [_h : EuclidGeom.PtNe B A] (Co : EuclidGeom.Collinear A B C) : EuclidGeom.lies_on C (DLIN A B)

If $A$, $B$ and $C$ are three collinear points in which $A \neq B$, then $C$ lies on the directed line associated to $AB$.

theorem EuclidGeom.DirLine.maximal {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} {C : P} (h₁ : EuclidGeom.lies_on A l) (h₂ : EuclidGeom.lies_on B l) [_h : EuclidGeom.PtNe B A] (Co : EuclidGeom.Collinear A B C) : EuclidGeom.lies_on C l

Given two points $A$ and $B$ on a directed line $l$, if a point $C$ is so that $A$, $B$, and $C$ are collinear, then $C$ lies on $l$.

theorem EuclidGeom.DirLine.lies_on_dirline_of_pt_pt_iff_collinear {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] (X : P) : EuclidGeom.lies_on X (DLIN A B) ↔ EuclidGeom.Collinear A B X

Given two distinct points $A$ and $B$, a point $X$ lies on the directed line from $A$ to $B$ if and only if $A$, $B$, and $X$ are collinear.

theorem EuclidGeom.DirLine.lies_on_iff_collinear_of_ne_lies_on_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} [_h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) (C : P) : EuclidGeom.lies_on C l ↔ EuclidGeom.Collinear A B C

Let $A$ and $B$ be two distinct points on a directed line $l$, then a point $C$ lies on $l$ if and only if $A$, $B$ and $C$ are collinear.

theorem EuclidGeom.collinear_iff_exist_dirLine_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) (C : P) : EuclidGeom.Collinear A B C ↔ ∃ (l : EuclidGeom.DirLine P), EuclidGeom.lies_on A l ∧ EuclidGeom.lies_on B l ∧ EuclidGeom.lies_on C l

The theorem states that three points $A$, $B$, and $C$ are collinear if and only if there exists a directed line $l$ such that $A$, $B$, and $C$ all lie on $l$.

theorem EuclidGeom.Line.exists_ne_pt_pt_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) {l : EuclidGeom.Line P} : ∃ (B : P), EuclidGeom.lies_on B l ∧ B ≠ A

There are two distinct points on a line, i.e. given a point $A$ on a line $l$, there exists a point $B$ on $l$ such that $B \neq A$.

theorem EuclidGeom.Line.lies_on_of_SegND_toProj_eq_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} (ha : EuclidGeom.lies_on A l) [_hab : EuclidGeom.PtNe B A] (hp : (SEG_nd A B).toProj = l.toProj) : EuclidGeom.lies_on B l

Given two distinct points $A$ and $B$, if $A$ lies on a line $l$ and the projective direction of segment $AB$ is the same as that of $l$, then $B$ lies on the $l$.

theorem EuclidGeom.Line.vec_vadd_pt_lies_on_line {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} (hA : EuclidGeom.lies_on A l) (hB : EuclidGeom.lies_on B l) [_h : EuclidGeom.PtNe B A] : EuclidGeom.lies_on (EuclidGeom.Vec.mkPtPt A B +ᵥ B) l

Let $A$ and $B$ be two distinct points on a line $l$, then moving $B$ by the vector $\xrightarrow{AB}$ still lies on $l$.

theorem EuclidGeom.Line.exist_pt_beyond_pt_right {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} (hA : EuclidGeom.lies_on A l) (hB : EuclidGeom.lies_on B l) [_h : EuclidGeom.PtNe B A] : ∃ (C : P), EuclidGeom.lies_on C l ∧ EuclidGeom.lies_int B { source := A, target := C }

Given two distinct points $A$ and $B$ on a line $l$, there exists a point $C$ on the line $l$ such that $B$ lies on the segment $AC$.

theorem EuclidGeom.Line.exist_pt_beyond_pt_left {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.Line P} (hA : EuclidGeom.lies_on A l) (hB : EuclidGeom.lies_on B l) [_h : EuclidGeom.PtNe B A] : ∃ (C : P), EuclidGeom.lies_on C l ∧ EuclidGeom.lies_int A { source := C, target := B }

Given two distinct points $A$ and $B$ on a line $l$, there exists some point $C$ on $l$ such that $A$ lies in the interior of the segment $CB$.

theorem EuclidGeom.DirLine.exists_ne_pt_pt_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) {l : EuclidGeom.DirLine P} : ∃ (B : P), EuclidGeom.lies_on B l ∧ B ≠ A

Given a point $A$ and a directed line $l$, there exists some point $B$ different from $A$ that lies on $l$.

theorem EuclidGeom.DirLine.lies_on_of_SegND_toProj_eq_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) [_hab : EuclidGeom.PtNe B A] (hp : (SEG_nd A B).toDir = l.toDir) : EuclidGeom.lies_on B l

Given two distinct points $A$ and $B$ and a directed line l, if $A$ lies on $l$ and the segment $AB$ is in the same direction as $l$, then $B$ lies on $l$.

theorem EuclidGeom.DirLine.exist_pt_beyond_pt_right {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} (hA : EuclidGeom.lies_on A l) (hB : EuclidGeom.lies_on B l) [_h : EuclidGeom.PtNe B A] : ∃ (C : P), EuclidGeom.lies_on C l ∧ EuclidGeom.lies_int B { source := A, target := C }

Given two distinct points $A$ and $B$ on a directed line $l$, there exists a point $C$ on $l$ such that $B$ lies in the interior of the segment AC.

theorem EuclidGeom.DirLine.exist_pt_beyond_pt_left {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {l : EuclidGeom.DirLine P} (hA : EuclidGeom.lies_on A l) (hB : EuclidGeom.lies_on B l) [_h : EuclidGeom.PtNe B A] : ∃ (C : P), EuclidGeom.lies_on C l ∧ EuclidGeom.lies_int A { source := C, target := B }

Let $A$ and $B$ be two distinct points that lie on a directed line $l$, then there exists a point $C$ on $l$ such that $A$ lies in the interior of segment $CB$.

@[inline, reducible]

abbrev EuclidGeom.DirLine.lelem {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) {l : EuclidGeom.DirLine P} (ha : EuclidGeom.lies_on A l) : ↑(EuclidGeom.DirLine.carrier l)

Equations

• EuclidGeom.DirLine.lelem A ha = { val := A, property := ha }

instance EuclidGeom.DirLine.instRealNormedAddTorsor {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) : NormedAddTorsor ℝ ↑(EuclidGeom.DirLine.carrier l)

A directed line can be viewed as a torsor over the addition group structure of $\mathbb{R}$, that is, points on a directed line can be translated by real multiples of the unit direction vector.

Equations

• EuclidGeom.DirLine.instRealNormedAddTorsor l = NormedAddTorsor.mk (_ : ∀ (h : ↑(EuclidGeom.DirLine.carrier l)) (y : ↑(EuclidGeom.DirLine.carrier l)), dist h y = ‖h -ᵥ y‖)

def EuclidGeom.DirLine.ddist {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : ℝ

Given two points $A$ and $B$ on a directed line $l$, this function returns the distance from $A$ to $B$ on the directed line $l$, as a real number; or in short $\dist(A, B)$.

Equations

• EuclidGeom.DirLine.ddist ha hb = EuclidGeom.DirLine.lelem B hb -ᵥ EuclidGeom.DirLine.lelem A ha

@[simp]

theorem EuclidGeom.DirLine.ddist_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} (ha : EuclidGeom.lies_on A l) : EuclidGeom.DirLine.ddist ha ha = 0

For a point $A$ on a directed line $l$, the distance from $A$ to itself is $0$, i.e. $\dist(A, A) = 0$.

@[simp]

theorem EuclidGeom.DirLine.neg_ddist_eq_ddist_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : -EuclidGeom.DirLine.ddist ha hb = EuclidGeom.DirLine.ddist hb ha

The negation of the distance from point $A$ to point $B$ on a directed line $l$ is equal to the distance from point $B$ to point $A$ on the same directed line $l$.

@[simp]

theorem EuclidGeom.DirLine.ddist_eq_zero_iff_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : EuclidGeom.DirLine.ddist ha hb = 0 ↔ B = A

The distance from point $A$ to point $B$ on a directed line $l$ is zero if and only if $B$ is equal to $A$.

@[simp]

theorem EuclidGeom.DirLine.ddist_ne_zero_iff_ne {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : EuclidGeom.DirLine.ddist ha hb ≠ 0 ↔ B ≠ A

The distance from point $A$ to point $B$ on directed line $l$ is non-zero if and only if $B$ is not equal to $A$.

@[simp]

theorem EuclidGeom.DirLine.ddist_add {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine 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.DirLine.ddist ha hb + EuclidGeom.DirLine.ddist hb hc = EuclidGeom.DirLine.ddist ha hc

Let $A$, $B$ and $C$ be three points on a directed line $l$. Then the sum of the distance from $A$ to $B$ and the distance from $B$ to $C$ is equal to the distance from $A$ to $C$, i.e. $\dist(A, B) + \dist(B, C) = \dist(A, C)$.

@[simp]

theorem EuclidGeom.DirLine.ddist_sub_right {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine 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.DirLine.ddist ha hb - EuclidGeom.DirLine.ddist ha hc = EuclidGeom.DirLine.ddist hc hb

On a directed line $l$, the distance from a point $A$ to point $B$ minus the distance from point $A$ to point $C$ is equal to the distance from point $C$ to point $B$.

@[simp]

theorem EuclidGeom.DirLine.ddist_sub_left {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine 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.DirLine.ddist ha hc - EuclidGeom.DirLine.ddist hb hc = EuclidGeom.DirLine.ddist ha hb

Given three points $A$, $B$, and $C$ on a directed line $l$, the difference between the distance from $A$ to $C$ and the distance from $B$ to $C$ is equal to the distance from $A$ to $B$.

@[simp]

theorem EuclidGeom.DirLine.ddist_left_cancel_iff {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine 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.DirLine.ddist ha hb = EuclidGeom.DirLine.ddist ha hc ↔ B = C

Given three points $A$, $B$, and $C$ on a directed line, the distance from point $A$ to point $B$ is equal to the distance from point $A$ to point $C$ if and only if point $B$ is the same as point $C$.

@[simp]

theorem EuclidGeom.DirLine.ddist_right_cancel_iff {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine 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.DirLine.ddist ha hc = EuclidGeom.DirLine.ddist hb hc ↔ A = B

On a directed line, the distance from point $A$ to point $C$ is equal to the distance from point $B$ to point $C$ if and only if $A$ is equal to $B$.

theorem EuclidGeom.DirLine.ddist_sub_ddist_comm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} {C : P} {D : P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) (hc : EuclidGeom.lies_on C l) (hd : EuclidGeom.lies_on D l) : EuclidGeom.DirLine.ddist ha hb - EuclidGeom.DirLine.ddist hc hd = EuclidGeom.DirLine.ddist hd hb - EuclidGeom.DirLine.ddist hc ha

Let $A$, $B$, $C$ and $D$ be four points on a directed line $l$. Then the distance from $A$ to $B$ minus the distance from $C$ to $D$ is equal to the distance from $D$ to $B$ minus the distance from $C$ to $A$, i.e $\dist(A, B) - \dist(C, D) = \dist(D, B) - \dist(C, A)$

theorem EuclidGeom.DirLine.ddist_add_ddist_comm {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} {C : P} {D : P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) (hc : EuclidGeom.lies_on C l) (hd : EuclidGeom.lies_on D l) : EuclidGeom.DirLine.ddist ha hb + EuclidGeom.DirLine.ddist hc hd = EuclidGeom.DirLine.ddist ha hd + EuclidGeom.DirLine.ddist hc hb

On a directed line, the sum of the distance from $A$ to $B$ and the distance from $C$ to $D$ is equal to the sum of the distance from $A$ to $D$ and the distance from $C$ to $B$.

theorem EuclidGeom.DirLine.pt_eq_ddist_smul_toDir_unitVec_vadd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : B = EuclidGeom.DirLine.ddist ha hb • l.toDir.unitVec +ᵥ A

theorem EuclidGeom.DirLine.vec_eq_ddist_smul_toDir_unitVec {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : EuclidGeom.Vec.mkPtPt A B = EuclidGeom.DirLine.ddist ha hb • l.toDir.unitVec

instance EuclidGeom.DirLine.instLinearOrderedAddTorsor {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.DirLine P) : LinearOrderedAddTorsor ℝ ↑(EuclidGeom.DirLine.carrier l)

Equations

• EuclidGeom.DirLine.instLinearOrderedAddTorsor l = AddTorsor.LinearOrderedAddTorsor_of_LinearOrderedAddCommGroup ℝ ↑(EuclidGeom.DirLine.carrier l)

theorem EuclidGeom.DirLine.le_iff_ddist_nonneg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : EuclidGeom.DirLine.lelem A ha ≤ EuclidGeom.DirLine.lelem B hb ↔ 0 ≤ EuclidGeom.DirLine.ddist ha hb

The theorem states that for two points $A$ and $B$ on a directed line $l$, we write $A \leq B$ if the distance from $A$ to $B$ is nonnegative.

theorem EuclidGeom.DirLine.lt_iff_ddist_pos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.DirLine P} {A : P} {B : P} (ha : EuclidGeom.lies_on A l) (hb : EuclidGeom.lies_on B l) : EuclidGeom.DirLine.lelem A ha < EuclidGeom.DirLine.lelem B hb ↔ 0 < EuclidGeom.DirLine.ddist ha hb

For two points $A$ and $B$ on a directed line $l$, $A$ is less than $B$ if and only if the distance from $A$ to $B$ is positive.