Segments and rays

In this file, we define the class of segments, rays, and their coercions, as well as basic properties. A more precise plan in terms of sections is as follows:

• (1) (definition) We define the corresponding classes: rays, segments, and nondegenerate segments.
• (2) (make) We define the make functions of rays, segments, and nondegenerate segments.
• (3) (coercion) We define the coercions among rays, segments, and nondegenerate segments, as well as coercions to directions, or projective directions.
• (4) (coercion-compatibility) We discuss compatibility of coercion functions.
• (5) (lieson-compatibility) We discuss compatibility regarding points lying on or in the interior of segments or rays.
• (6) (reverse) We introduce the concept of reversing a segment and reversing a ray.
• (7) (extension) We define the extension ray of a nondegenerate segment.
• (8) (length) We define the length function of a segment.
• (9) (midpoint) We define the function that gives the midpoint of a segment.
• (10) (archimedean) We discuss the Archimedean property of a segment.

Important definitions

• Class Ray : A \emph{ray} consists of the pair of its source point $P$ and its direction.
• Class Seg : A \emph{segment} consists of a pair of points: the source and the target. (We allow the source and the target to be the same.)
• Subclass SegND : A \emph{nondegenerate segment} is a segment whose source and target are not equal.
• Definition Seg.length : The function that gives the length of a given segment.
• Definition Ray.reverse : Given a ray, this function returns the ray with the same source but with reversed direction.
• Definition Seg.reverse : Given a segment, this function swapped its source and target point.
• Definition SegND.reverse : Given a nondegenerate segment, this function swapped its source and target point.
• Definition SegND.extension : Given a nondegenerate segment, this function returns the extension ray of the segment.
• Definition Seg.midpoint : This function returns the hmidpoint of a segment.

List of notations

• SEG A B : notation for the segment with source $A$ and target $B$.
• SEG_nd A B : notation for the segment with source $A$ and target $B$, where $h$ is a proof of that $A \neq B$.
• RAY A B h : notation for the ray with source $A$ in the direction of $B$, where $h$ is a proof of that $A \neq B$.

List of main theorems

Implementation notes

Further works

(1) Definition

theorem EuclidGeom.Ray.ext_iff {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Ray P), x = y ↔ x.source = y.source ∧ x.toDir = y.toDir

theorem EuclidGeom.Ray.ext {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Ray P), x.source = y.source → x.toDir = y.toDir → x = y

structure EuclidGeom.Ray (P : Type u_1) [EuclidGeom.EuclideanPlane P] : Type u_1

A \emph{ray} consists of a pair of a point $P$ and a direction; it is the ray that starts at the point and extends in the given direction.

• source : P

  returns the source of the ray.

• toDir : EuclidGeom.Dir

  returns the direction of the ray.

def EuclidGeom.Ray.mk_pt_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (source : P) (toDir : EuclidGeom.Dir) : EuclidGeom.Ray P

Alias of EuclidGeom.Ray.mk.

Equations

• @EuclidGeom.Ray.mk_pt_dir = @EuclidGeom.Ray.mk

theorem EuclidGeom.Seg.ext_iff {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Seg P), x = y ↔ x.source = y.source ∧ x.target = y.target

theorem EuclidGeom.Seg.ext {P : Type u_1} : ∀ {inst : EuclidGeom.EuclideanPlane P} (x y : EuclidGeom.Seg P), x.source = y.source → x.target = y.target → x = y

structure EuclidGeom.Seg (P : Type u_1) [EuclidGeom.EuclideanPlane P] : Type u_1

A \emph{Segment} consists of a pair of points: the source and the target; it is the segment from the source to the target. (We allow the source and the target to be the same.)

• source : P

  returns the source of the segment.

• target : P

  returns the target of the segment.

def EuclidGeom.Seg.IsND {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg : EuclidGeom.Seg P) : Prop

Given a segment $AB$, this function returns whether the segment $AB$ is nondegenerate, i.e. whether $A \neq B$.

Equations

• EuclidGeom.Seg.IsND seg = (seg.target ≠ seg.source)

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

A \emph{nondegenerate segment} is a segment $AB$ that is nondegenerate, i.e. $A \neq B$.

Equations

• EuclidGeom.SegND P = { seg : EuclidGeom.Seg P // EuclidGeom.Seg.IsND seg }

(2) Make

def EuclidGeom.termSEG : Lean.ParserDescr

Given two points $A$ and $B$, this returns the segment with source $A$ and target $B$. It is an abbreviation of $\verb|Seg.mk|$.

Equations

• EuclidGeom.termSEG = Lean.ParserDescr.node `EuclidGeom.termSEG 1024 (Lean.ParserDescr.symbol "SEG")

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

Given two distinct points $A$ and $B$, this function returns a nondegenerate segment with source $A$ and target $B$. We use $\verb|SEG_nd|$ to abbreviate $\verb|SegND.mk|$.

Equations

• SEG_nd A B h = { val := { source := A, target := B }, property := h }

def EuclidGeom.termSEG_nd______ : Lean.ParserDescr

Given two distinct points $A$ and $B$, this function returns a nondegenerate segment with source $A$ and target $B$. We use $\verb|SEG_nd|$ to abbreviate $\verb|SegND.mk|$.

Equations

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

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

Delaborator for SegND.mk

Equations

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

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

Given two distinct points $A$ and $B$, this function returns the ray starting from $A$ in the direction of $B$. By definition, the direction of the ray is given by the normalization of the vector from $A$ to $B$, using $\verb|toDir|$ function. We use $\verb|RAY|$ to abbreviate $\verb|Ray.mk_pt_pt|$.

Equations

• RAY A B h = { source := A, toDir := { val := EuclidGeom.Vec.mkPtPt A B, property := (_ : B -ᵥ A ≠ 0) }.toDir }

def EuclidGeom.termRAY______ : Lean.ParserDescr

Given two distinct points $A$ and $B$, this function returns the ray starting from $A$ in the direction of $B$. By definition, the direction of the ray is given by the normalization of the vector from $A$ to $B$, using $\verb|toDir|$ function. We use $\verb|RAY|$ to abbreviate $\verb|Ray.mk_pt_pt|$.

Equations

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

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

Delaborator for Ray.mk_pt_pt

Equations

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

(3) Coersion

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

Given a ray, this function returns its projective direction; it is the projective direction of the direction of the ray.

Equations

• ray.toProj = ray.toDir.toProj

def EuclidGeom.Ray.IsOn {P : Type u_1} [EuclidGeom.EuclideanPlane P] (X : P) (ray : EuclidGeom.Ray P) : Prop

Given a point $X$ and a ray $ray$, this function returns whether $X$ lies on $ray$; here saying that $X$ lies on $ray$ means that the vector from the start point of the ray to $X$ is some nonnegative multiple of the direction vector of the ray.

Equations

• EuclidGeom.Ray.IsOn X ray = ∃ (t : ℝ), 0 ≤ t ∧ EuclidGeom.Vec.mkPtPt ray.source X = t • ray.toDir.unitVec

structure EuclidGeom.Ray.IsInt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (X : P) (ray : EuclidGeom.Ray P) : Prop

Given a point $X$ and a ray, this function returns whether the point lies in the interior of the ray; here saying that a point lies in the interior of a ray means that it lies on the ray and is not equal to the source of the ray.

• isOn : EuclidGeom.Ray.IsOn X ray
• ne_source : X ≠ ray.source

def EuclidGeom.Ray.ne_source_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {ray : EuclidGeom.Ray P} (self : EuclidGeom.Ray.IsInt X ray) : X ≠ ray.source

Alias of EuclidGeom.Ray.IsInt.ne_source.

Equations

• @EuclidGeom.Ray.ne_source_of_lies_int = @EuclidGeom.Ray.IsInt.ne_source

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

Given a ray, its carrier is the set of points that lie on the ray.

Equations

• EuclidGeom.Ray.carrier ray = {X : P | EuclidGeom.Ray.IsOn X ray}

def EuclidGeom.Ray.interior {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray : EuclidGeom.Ray P) : Set P

Given a ray, its interior is the set of points that lie in the interior of the ray.

Equations

• EuclidGeom.Ray.interior ray = {X : P | EuclidGeom.Ray.IsInt X ray}

instance EuclidGeom.Ray.instIntFigRay {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.IntFig (EuclidGeom.Ray P) P

This is to register that a ray is an instance of a class of objects that we may speak of both carrier and interior (and that the interior is a subset of the carrier).

Equations

• EuclidGeom.Ray.instIntFigRay = EuclidGeom.IntFig.mk (_ : ∀ (x : EuclidGeom.Ray P) (x_1 : P), EuclidGeom.Ray.IsInt x_1 x → EuclidGeom.Ray.IsOn x_1 x)

def EuclidGeom.Seg.toVec {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg : EuclidGeom.Seg P) : EuclidGeom.Vec

Given a segment, this function returns the vector associated to the segment, that is, the vector from the source of the segment to the target of the segment.

Equations

• seg.toVec = EuclidGeom.Vec.mkPtPt seg.source seg.target

@[simp]

theorem EuclidGeom.Seg.mk_source_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] (s : EuclidGeom.Seg P) : EuclidGeom.Vec.mkPtPt s.source s.target = s.toVec

def EuclidGeom.Seg.IsOn {P : Type u_1} [EuclidGeom.EuclideanPlane P] (X : P) (seg : EuclidGeom.Seg P) : Prop

Given a point $X$ and a segment $seg$, this function returns whether $X$ lies on $seg$; here saying that $X$ lies on $seg$ means that the vector from the source of $seg$ to $X$ is a real multiple $t$ of the vector of $seg$ with $0 \leq t \leq 1$.

Equations

• EuclidGeom.Seg.IsOn X seg = ∃ (t : ℝ), 0 ≤ t ∧ t ≤ 1 ∧ EuclidGeom.Vec.mkPtPt seg.source X = t • EuclidGeom.Vec.mkPtPt seg.source seg.target

structure EuclidGeom.Seg.IsInt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (X : P) (seg : EuclidGeom.Seg P) : Prop

Given a point $X$ and a segment $seg$, this function returns whether $X$ lies in the interior of $seg$; here saying that $X$ lies in the interior of $seg$ means $X$ lies on $seg$ and is different from the source and the target of $seg$.

• isOn : EuclidGeom.Seg.IsOn X seg
• ne_source : X ≠ seg.source
• ne_target : X ≠ seg.target

def EuclidGeom.Seg.ne_source_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg : EuclidGeom.Seg P} (self : EuclidGeom.Seg.IsInt X seg) : X ≠ seg.source

Alias of EuclidGeom.Seg.IsInt.ne_source.

Equations

• @EuclidGeom.Seg.ne_source_of_lies_int = @EuclidGeom.Seg.IsInt.ne_source

def EuclidGeom.Seg.ne_target_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg : EuclidGeom.Seg P} (self : EuclidGeom.Seg.IsInt X seg) : X ≠ seg.target

Alias of EuclidGeom.Seg.IsInt.ne_target.

Equations

• @EuclidGeom.Seg.ne_target_of_lies_int = @EuclidGeom.Seg.IsInt.ne_target

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

Given a segment, this function returns the set of points that lie on the segment.

Equations

• EuclidGeom.Seg.carrier seg = {X : P | EuclidGeom.Seg.IsOn X seg}

def EuclidGeom.Seg.interior {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg : EuclidGeom.Seg P) : Set P

Given a segment, this function returns the set of points that lie in the interior of the segment.

Equations

• EuclidGeom.Seg.interior seg = {X : P | EuclidGeom.Seg.IsInt X seg}

instance EuclidGeom.Seg.instIntFigSeg {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.IntFig (EuclidGeom.Seg P) P

Instance $\verb|IntFig Seg|$ : This is to register that a segment is an instance of a class of objects that we may speak of both carrier and interior (and that the interior is a subset of the carrier).

Equations

• EuclidGeom.Seg.instIntFigSeg = EuclidGeom.IntFig.mk (_ : ∀ (x : EuclidGeom.Seg P), ∀ x_1 ∈ EuclidGeom.Interior.interior x, EuclidGeom.Seg.IsOn x_1 x)

instance EuclidGeom.SegND.instCoeSegNDSeg {P : Type u_1} [EuclidGeom.EuclideanPlane P] : Coe (EuclidGeom.SegND P) (EuclidGeom.Seg P)

One may naturally coerce a nondegenerate segment into a segment.

Equations

• EuclidGeom.SegND.instCoeSegNDSeg = { coe := fun (x : EuclidGeom.SegND P) => ↑x }

@[inline, reducible]

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

Given a nondegenerate segment, this function returns the source of the segment.

Equations

• seg_nd.source = (↑seg_nd).source

@[inline, reducible]

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

Given a nondegenerate segment, this function returns the target of the segment.

Equations

• seg_nd.target = (↑seg_nd).target

def EuclidGeom.SegND.toVecND {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg_nd : EuclidGeom.SegND P) : EuclidGeom.VecND

Given a nondegenerate segment $AB$, this function returns the nondegenerate vector $\overrightarrow{AB}$.

Equations

• seg_nd.toVecND = { val := EuclidGeom.Vec.mkPtPt seg_nd.source seg_nd.target, property := (_ : EuclidGeom.Vec.mkPtPt seg_nd.source seg_nd.target ≠ 0) }

@[inline, reducible]

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

Given a nondegenerate segment $AB$, this function returns the direction associated to the segment, defined by normalizing the nondegenerate vector $\overrightarrow{AB}$.

Equations

• seg_nd.toDir = seg_nd.toVecND.toDir

def EuclidGeom.SegND.toRay {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg_nd : EuclidGeom.SegND P) : EuclidGeom.Ray P

Given a nondegenerate segment $AB$, this function returns the ray $AB$, whose source is $A$ in the direction of $B$.

Equations

• seg_nd.toRay = { source := (↑seg_nd).source, toDir := seg_nd.toDir }

@[simp]

theorem EuclidGeom.SegND.toRay_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] (s : EuclidGeom.SegND P) : s.toRay.source = s.source

@[inline, reducible]

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

Given a nondegenerate segment $AB$, this function returns the projective direction of $AB$, defined as the projective direction of the nondegenerate vector $\overrightarrow{AB}$.

Equations

• seg_nd.toProj = seg_nd.toVecND.toProj

@[inline, reducible]

abbrev EuclidGeom.SegND.IsOn {P : Type u_1} [EuclidGeom.EuclideanPlane P] (X : P) (seg_nd : EuclidGeom.SegND P) : Prop

Given a point $A$ and a nondegenerate segment $seg_nd$, this function returns whether $A$ lies on $seg_nd$, namely, whether it lies on the corresponding segment.

Equations

• EuclidGeom.SegND.IsOn X seg_nd = EuclidGeom.Seg.IsOn X ↑seg_nd

@[inline, reducible]

abbrev EuclidGeom.SegND.IsInt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (X : P) (seg_nd : EuclidGeom.SegND P) : Prop

Given a point $A$ and a nondegenerate segment $seg_nd$, this function returns whether $A$ lies in the interior of $seg_nd$, namely, whether it lies in the interior of the corresponding segment.

Equations

• EuclidGeom.SegND.IsInt X seg_nd = EuclidGeom.Seg.IsInt X ↑seg_nd

@[inline, reducible]

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

Given a nondegenerate segment, this function returns the set of points that lie on the segment.

Equations

• EuclidGeom.SegND.carrier seg_nd = {X : P | EuclidGeom.SegND.IsOn X seg_nd}

@[inline, reducible]

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

Given a nondegenerate segment, this function returns the set of points that lie in the interior of the segment.

Equations

• EuclidGeom.SegND.interior seg_nd = {X : P | EuclidGeom.Seg.IsInt X ↑seg_nd}

instance EuclidGeom.SegND.instIntFigSegND {P : Type u_1} [EuclidGeom.EuclideanPlane P] : EuclidGeom.IntFig (EuclidGeom.SegND P) P

This is to register that a nondegenerate segment is an instance of a class of objects that we may speak of both carrier and interior (and that the interior is a subset of the carrier).

Equations

• EuclidGeom.SegND.instIntFigSegND = EuclidGeom.IntFig.mk (_ : ∀ (x : EuclidGeom.SegND P), ∀ x_1 ∈ EuclidGeom.Interior.interior x, EuclidGeom.Seg.IsOn x_1 ↑x)

@[simp]

theorem EuclidGeom.Ray.mkPtPt_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) [_h : EuclidGeom.PtNe B A] : (RAY A B).toDir = (VEC_nd A B).toDir

@[simp]

theorem EuclidGeom.SegND.mkPtPt_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) [_h : EuclidGeom.PtNe B A] : (SEG_nd A B).toDir = (VEC_nd A B).toDir

(4) Coersion compatiblity

@[simp]

theorem EuclidGeom.SegND.toRay_toDir_eq_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : seg_nd.toRay.toDir = seg_nd.toDir

Given a nondegenerate segment, the direction of to the ray associated to the segment is the same as the direction of the segment.

@[simp]

theorem EuclidGeom.SegND.toRay_toProj_eq_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : seg_nd.toProj = seg_nd.toProj

Given a nondegenerate segment, the projective direction of the ray associated to the segment is the same as the projective direction of the segment.

@[simp]

theorem EuclidGeom.seg_toVec_eq_vec {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} : { source := A, target := B }.toVec = EuclidGeom.Vec.mkPtPt A B

Given two points $A$ and $B$, the vector associated to the segment $AB$ is same as vector $\overrightarrow{AB}$.

theorem EuclidGeom.toVec_eq_zero_of_deg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.Seg P} : l.target = l.source ↔ l.toVec = 0

Given a segment $AB$, $A$ is same as $B$ if and only if vector $\overrightarrow{AB}$ is zero.

theorem EuclidGeom.Ray.toDir_eq_neg_toDir_of_mk_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [h : EuclidGeom.PtNe B A] : (RAY A B).toDir = -(RAY B A).toDir

Given two distinct points $A$ and $B$, the direction of ray $AB$ is same as the negative direction of ray $BA$

theorem EuclidGeom.Ray.toProj_eq_toProj_of_mk_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : (RAY A B).toProj = (RAY B A).toProj

Given two distinct points $A$ and $B$, the projective direction of ray $AB$ is same as that of ray $BA$.

theorem EuclidGeom.pt_pt_seg_toRay_eq_pt_pt_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : (SEG_nd A B).toRay = RAY A B

Given two distinct points $A$ and $B$, the ray associated to the segment $AB$ is same as ray $AB$.

theorem EuclidGeom.Seg.IsND_iff_toVec_ne_zero {P : Type u_1} [EuclidGeom.EuclideanPlane P] {l : EuclidGeom.Seg P} : EuclidGeom.Seg.IsND l ↔ l.toVec ≠ 0

Given a segment $AB$, $AB$ is nondegenerate if and only if vector $\overrightarrow{AB}$ is nonzero.

theorem EuclidGeom.dir_parallel_of_same_proj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray₁ : EuclidGeom.Ray P} {ray₂ : EuclidGeom.Ray P} (h : ray₁.toProj = ray₂.toProj) : ∃ (t : ℝ), ray₂.toDir.unitVec = t • ray₁.toDir.unitVec

If $ray_1$ and $ray_2$ are two rays with the same projective direction, then the direction vector of $ray_2$ is a real multiple of the direction vector of $ray_1$.

(5) Lieson compatibility

@[simp]

theorem EuclidGeom.SegND.lies_on_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_on X seg_nd ↔ EuclidGeom.lies_on X ↑seg_nd

Given a nondegenerate segment, a point lies on the nondegenerate segment if and only if it lies on the corresponding segment (without knowing the nondegenate condition).

@[simp]

theorem EuclidGeom.SegND.lies_int_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_int X seg_nd ↔ EuclidGeom.lies_int X ↑seg_nd

Given a nondegenerate segment, a point lies in the interior of the nondegenerate segment if and only if it lies in the interior of the corresponding segment (without knowing the nondegenate condition).

theorem EuclidGeom.Ray.lies_on_iff {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {ray : EuclidGeom.Ray P} : EuclidGeom.lies_on X ray ↔ ∃ (t : ℝ), 0 ≤ t ∧ EuclidGeom.Vec.mkPtPt ray.source X = t • ray.toDir.unitVec

Given a ray, a point $X$ lies on the ray if and only if the vector from the source of the ray to $X$ is a nonnegative multiple of the direction of ray.

theorem EuclidGeom.Ray.lies_int_iff {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {ray : EuclidGeom.Ray P} : EuclidGeom.lies_int X ray ↔ ∃ (t : ℝ), 0 < t ∧ EuclidGeom.Vec.mkPtPt ray.source X = t • ray.toDir.unitVec

Given a ray, a point $X$ lies in the interior of the ray if and only if the vector from the source of the ray to $X$ is a positive multiple of the direction of ray.

theorem EuclidGeom.SegND.lies_on_iff {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_on X seg_nd ↔ ∃ (t : ℝ), 0 ≤ t ∧ t ≤ 1 ∧ EuclidGeom.Vec.mkPtPt seg_nd.source X = t • ↑seg_nd.toVecND

For a nondegenerate segment $AB$, a point $X$ lies on $AB$ if and only if there exist a real number $t$ satisfying that $0 \leq t \leq 1$ and that the vector $\overrightarrow{AX}$ is same as $t \cdot \overrightarrow{AB}$.

theorem EuclidGeom.SegND.lies_int_iff {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_int X seg_nd ↔ ∃ (t : ℝ), 0 < t ∧ t < 1 ∧ EuclidGeom.Vec.mkPtPt seg_nd.source X = t • ↑seg_nd.toVecND

For a nondegenerate segment $AB$, a point $X$ lies in the interior of $AB$ if and only if there exist a real number $t$ satisfying that $0 < t < 1$ and that the vector $\overrightarrow{AX}$ is same as $t \cdot \overrightarrow{AB}$.

theorem EuclidGeom.SegND.ne_source_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_int X s) : X ≠ s.source

For a nondegenerate segment $AB$, if a point $X$ lies on the interior of $AB$ then $X$ not equal to $A$.

theorem EuclidGeom.SegND.ne_target_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {s : EuclidGeom.SegND P} (h : EuclidGeom.lies_int X s) : X ≠ s.target

For a nondegenerate segment $AB$, if a point $X$ lies on the interior of $AB$ then $X$ not equal to $B$.

theorem EuclidGeom.Seg.isND_of_pt_liesint {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} {X : P} (h : EuclidGeom.lies_int X seg) : EuclidGeom.Seg.IsND seg

For a segment $AB$, if there exists an interior point $X$, then it is nondegenerate.

theorem EuclidGeom.Seg.lies_int_iff {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg : EuclidGeom.Seg P} : EuclidGeom.lies_int X seg ↔ EuclidGeom.Seg.IsND seg ∧ ∃ (t : ℝ), 0 < t ∧ t < 1 ∧ EuclidGeom.Vec.mkPtPt seg.source X = t • seg.toVec

For a segment $AB$, a point $X$ lies in the interior of $AB$ if and only if $AB$ is nondegenerate, and there exist a real number $t$ satisfying that $0 < t < 1$ and that the vector $\overrightarrow{AX}$ is same as $t \cdot \overrightarrow{AB}$.

@[simp]

theorem EuclidGeom.Seg.source_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : EuclidGeom.lies_on seg.source seg

Given a segment $AB$, the source $A$ of the segment lies on the segment.

@[simp]

theorem EuclidGeom.Seg.target_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : EuclidGeom.lies_on seg.target seg

Given a segment $AB$, the target $B$ lies on the segment $AB$.

@[simp]

theorem EuclidGeom.Seg.source_not_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : ¬EuclidGeom.lies_int seg.source seg

Given a segment $AB$, the source $A$ does not belong to the interior of $AB$.

@[simp]

theorem EuclidGeom.Seg.target_not_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : ¬EuclidGeom.lies_int seg.target seg

Given a segment $AB$, the target $B$ does not belong to the interior of $AB$.

@[simp]

theorem EuclidGeom.Seg.lies_on_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg : EuclidGeom.Seg P} (h : EuclidGeom.lies_int X seg) : EuclidGeom.lies_on X seg

For a segment $AB$, every point of the interior of $AB$ lies on the segment $AB$.

@[simp]

theorem EuclidGeom.SegND.source_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_on seg_nd.source seg_nd

Given a nondegenerate segment $AB$, the source $A$ of the segment lies on the segment.

@[simp]

theorem EuclidGeom.SegND.target_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_on seg_nd.target seg_nd

Given a nondegenerate segment $AB$, the target $B$ lies on the segment $AB$.

@[simp]

theorem EuclidGeom.SegND.source_not_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : ¬EuclidGeom.lies_int seg_nd.source seg_nd

Given a nondegenerate segment $AB$, the source $A$ does not belong to the interior of $AB$.

@[simp]

theorem EuclidGeom.SegND.target_not_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : ¬EuclidGeom.lies_int seg_nd.target seg_nd

Given a nondegenerate segment $AB$, the target $B$ does not belong to the interior of $AB$.

@[simp]

theorem EuclidGeom.SegND.lies_on_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} (h : EuclidGeom.lies_int X seg_nd) : EuclidGeom.lies_on X seg_nd

For a nondegenerate segment $AB$, every point of the interior of $AB$ lies on the segment $AB$.

@[simp]

theorem EuclidGeom.Ray.source_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} : EuclidGeom.lies_on ray.source ray

Given a ray, the source of the ray lies on the ray.

@[simp]

theorem EuclidGeom.Ray.source_not_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} : ¬EuclidGeom.lies_int ray.source ray

Given a ray, the source of the ray does not lie in the interior of the ray.

@[simp]

theorem EuclidGeom.Ray.lies_on_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {ray : EuclidGeom.Ray P} (h : EuclidGeom.lies_int X ray) : EuclidGeom.lies_on X ray

For a ray, every point of the interior of the ray lies on the ray.

theorem EuclidGeom.Ray.lies_int_def {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {ray : EuclidGeom.Ray P} : EuclidGeom.lies_int X ray ↔ EuclidGeom.lies_on X ray ∧ X ≠ ray.source

Given a ray, a point lies in the interior of the ray if and only if it lies on the ray and is different from the source of ray.

theorem EuclidGeom.SegND.lies_on_toRay_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} (h : EuclidGeom.lies_on X seg_nd) : EuclidGeom.lies_on X seg_nd.toRay

For a nondegenerate segment $AB$, every point of the segment $AB$ lies on the ray associated to $AB$.

theorem EuclidGeom.SegND.lies_int_toRay_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} (h : EuclidGeom.lies_int X seg_nd) : EuclidGeom.lies_int X seg_nd.toRay

For a nondegenerate segment $seg_nd$, every point of the interior of the $seg_nd$ lies in the interior of the ray associated to the $seg_nd$.

theorem EuclidGeom.SegND.target_lies_int_toRay {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_int seg_nd.target seg_nd.toRay

Given a nondegenerate segment $seg_nd$, the target of $seg_nd$ lies on the interior of the ray associated to $seg_nd$

theorem EuclidGeom.Ray.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 (RAY A B)

Given two distinct points $A$ and $B$, $B$ lies on the ray $AB$.

theorem EuclidGeom.Ray.snd_pt_lies_int_mk_pt_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (A : P) (B : P) [h : EuclidGeom.PtNe B A] : EuclidGeom.lies_int B (RAY A B)

Given two distinct points $A$ and $B$, $B$ lies in the interior of the ray $AB$.

theorem EuclidGeom.Ray.pt_pt_toDir_eq_ray_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} {A : P} (h : EuclidGeom.lies_int A ray) : (RAY ray.source A (_ : A ≠ ray.source)).toDir = ray.toDir

Given a point $A$ on a ray, the direction of the ray is the same as the direction from the source of the ray to $A$.

theorem EuclidGeom.Ray.pt_pt_eq_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} {A : P} (h : EuclidGeom.lies_int A ray) : RAY ray.source A (_ : A ≠ ray.source) = ray

Given a point $A$ on the interior of a ray, the ray starting at the source of the ray in the direction of $A$ is the same as the original ray.

theorem EuclidGeom.Ray.source_int_toRay_eq_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} {A : P} (h : EuclidGeom.lies_int A ray) : (SEG_nd ray.source A (_ : A ≠ ray.source)).toRay = ray

Given a point $A$ on the interior of a ray, the ray associated to the segment from the source of the ray to $A$ is the same as the original ray.

theorem EuclidGeom.Ray.vec_eq_dist_smul_toDir_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {r : EuclidGeom.Ray P} (h : EuclidGeom.lies_on A r) : EuclidGeom.Vec.mkPtPt r.source A = dist r.source A • r.toDir.unitVec

Given a point $A$ on the interior of a ray, the vector from the source of the ray to $A$ is equal to the distance of the source and $A$ times the direction vector of the original ray.

theorem EuclidGeom.every_pt_lies_on_seg_of_source_and_target_lies_on_seg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg₁ : EuclidGeom.Seg P} {seg₂ : EuclidGeom.Seg P} (h₁ : EuclidGeom.lies_on seg₁.source seg₂) (h₂ : EuclidGeom.lies_on seg₁.target seg₂) {A : P} (ha : EuclidGeom.lies_on A seg₁) : EuclidGeom.lies_on A seg₂

Given two segments $seg_1$ and $seg_2$, if the source and the target of the $seg_1$ both lie on $seg_2$, then every point of $seg_1$ lies on $seg_2$.

theorem EuclidGeom.every_pt_lies_int_seg_of_source_and_target_lies_int_seg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg₁ : EuclidGeom.Seg P} {seg₂ : EuclidGeom.Seg P} (h₁ : EuclidGeom.lies_int seg₁.source seg₂) (h₂ : EuclidGeom.lies_int seg₁.target seg₂) {A : P} (ha : EuclidGeom.lies_on A seg₁) : EuclidGeom.lies_int A seg₂

Given two segments $seg_1$ and $seg_2$, if the source and the target of $seg_1$ both lie in the interior of $seg_2$, and if $A$ is a point on $seg_1$, then $A$ lies in the interior of $seg_2$.

theorem EuclidGeom.every_int_pt_lies_int_seg_of_source_and_target_lies_on_seg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg₁ : EuclidGeom.Seg P} {seg₂ : EuclidGeom.Seg P} (h₁ : EuclidGeom.lies_on seg₁.source seg₂) (h₂ : EuclidGeom.lies_on seg₁.target seg₂) {A : P} (ha : EuclidGeom.lies_int A seg₁) : EuclidGeom.lies_int A seg₂

Given two segments $seg_1$ and $seg_2$, if the source and the target of $seg_1$ both lie on $seg_2$, and if $A$ is a point in the interior of $seg_1$, then $A$ lies in the interior of $seg_2$.

theorem EuclidGeom.every_pt_lies_on_ray_of_source_and_target_lies_on_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} {ray : EuclidGeom.Ray P} (h₁ : EuclidGeom.lies_on seg.source ray) (h₂ : EuclidGeom.lies_on seg.target ray) {A : P} (ha : EuclidGeom.lies_on A seg) : EuclidGeom.lies_on A ray

Given a segment and a ray, if the source and the target of the segment both lie on the ray, and if $A$ is a point on the segment, then $A$ lies on the ray.

theorem EuclidGeom.every_pt_lies_int_ray_of_source_and_target_lies_int_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} {ray : EuclidGeom.Ray P} (h₁ : EuclidGeom.lies_int seg.source ray) (h₂ : EuclidGeom.lies_int seg.target ray) {A : P} (ha : EuclidGeom.lies_on A seg) : EuclidGeom.lies_int A ray

Given a segment and a ray, if the source and the target of the segment both lie in the interior of the ray, and if $A$ is a point on the segment, then $A$ lies in the interior of the ray.

theorem EuclidGeom.every_int_pt_lies_int_ray_of_source_and_target_lies_on_ray {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} {ray : EuclidGeom.Ray P} (h₁ : EuclidGeom.lies_on seg.source ray) (h₂ : EuclidGeom.lies_on seg.target ray) {A : P} (ha : EuclidGeom.lies_int A seg) : EuclidGeom.lies_int A ray

Given a segment and a ray, if the source and the target of the segment both lie on the ray, and if $A$ is a point in the interior of the segment, then $A$ lies in the interior of the ray.

theorem EuclidGeom.every_pt_lies_on_ray_of_source_lies_on_ray_and_same_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray₁ : EuclidGeom.Ray P} {ray₂ : EuclidGeom.Ray P} (e : ray₁.toDir = ray₂.toDir) (h : EuclidGeom.lies_on ray₁.source ray₂) {A : P} (ha : EuclidGeom.lies_on A ray₁) : EuclidGeom.lies_on A ray₂

Given two rays $ray_1$ and $ray_2$ with same direction, if the source of $ray_1$ lies on $ray_2$, and if $A$ is a point on $ray_1$, then $A$ lies on $ray_2$.

theorem EuclidGeom.every_pt_lies_int_ray_of_source_lies_int_ray_and_same_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray₁ : EuclidGeom.Ray P} {ray₂ : EuclidGeom.Ray P} (e : ray₁.toDir = ray₂.toDir) (h : EuclidGeom.lies_int ray₁.source ray₂) {A : P} (ha : EuclidGeom.lies_on A ray₁) : EuclidGeom.lies_int A ray₂

Given two rays $ray_1$ and $ray_2$ with same direction, if the source of $ray_1$ lies in the interior of $ray_2$, and if $A$ is a point on $ray_1$, then $A$ lies in the interior of $ray_2$.

theorem EuclidGeom.SegND.source_pt_toDir_eq_toDir_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} {A : P} (h : EuclidGeom.lies_int A seg_nd) : (SEG_nd seg_nd.source A (_ : A ≠ (↑seg_nd).source)).toDir = seg_nd.toDir

Given a nondegenerate segment $Segnd$ and a point $A$ lies in the interior of it. Then the direction of the nondegenerate segment from the source of $Segnd$ to $A$ equals the direction of $Segnd$.

theorem EuclidGeom.Ray.lies_int_iff_pos_of_vec_eq_smul_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} {A : P} {t : ℝ} (h : EuclidGeom.Vec.mkPtPt ray.source A = t • ray.toDir.unitVec) : EuclidGeom.lies_int A ray ↔ 0 < t

theorem EuclidGeom.Ray.eq_source_iff_eq_zero_of_vec_eq_smul_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} {A : P} {t : ℝ} (h : EuclidGeom.Vec.mkPtPt ray.source A = t • ray.toDir.unitVec) : A = ray.source ↔ t = 0

(6) Reverse

@[simp]

theorem EuclidGeom.Ray.reverse_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray : EuclidGeom.Ray P) : ray.reverse.source = ray.source

@[simp]

theorem EuclidGeom.Ray.reverse_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray : EuclidGeom.Ray P) : ray.reverse.toDir = -ray.toDir

def EuclidGeom.Ray.reverse {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray : EuclidGeom.Ray P) : EuclidGeom.Ray P

Given a ray, this function returns the ray with the same source but with reversed direction.

Equations

• ray.reverse = { source := ray.source, toDir := -ray.toDir }

@[simp]

theorem EuclidGeom.Seg.reverse_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg : EuclidGeom.Seg P) : seg.reverse.target = seg.source

@[simp]

theorem EuclidGeom.Seg.reverse_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg : EuclidGeom.Seg P) : seg.reverse.source = seg.target

def EuclidGeom.Seg.reverse {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg : EuclidGeom.Seg P) : EuclidGeom.Seg P

Given a segment $AB$, this function returns its reverse, i.e. the segment $BA$.

Equations

• seg.reverse = { source := seg.target, target := seg.source }

@[simp]

theorem EuclidGeom.seg_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} : { source := A, target := B }.reverse = { source := B, target := A }

The reverse of segment $AB$ is the segment $BA$.

theorem EuclidGeom.nd_of_rev_of_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} (nd : EuclidGeom.Seg.IsND seg) : EuclidGeom.Seg.IsND seg.reverse

If a segment is nondegenerate, so is its reverse segment.

def EuclidGeom.SegND.reverse {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg_nd : EuclidGeom.SegND P) : EuclidGeom.SegND P

Given a nondegenerate segment $AB$, this function returns the reversed nondegenerate segment $BA$.

Equations

• EuclidGeom.SegND.reverse seg_nd = { val := (↑seg_nd).reverse, property := (_ : EuclidGeom.Seg.IsND (↑seg_nd).reverse) }

@[simp]

theorem EuclidGeom.seg_nd_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} [_h : EuclidGeom.PtNe B A] : EuclidGeom.SegND.reverse (SEG_nd A B) = SEG_nd B A

The reverse of a nondegenerate segment $AB$ is the nondegenerate segment $BA$.

@[simp]

theorem EuclidGeom.SegND.rev_toseg_eq_toseg_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : ↑(EuclidGeom.SegND.reverse seg_nd) = (↑seg_nd).reverse

Given a nondegenerate segment, first viewing it as a segment and then reversing it is the same as first reversing it and then viewing it as a segment.

@[simp]

theorem EuclidGeom.Ray.source_of_rev_eq_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} : ray.reverse.source = ray.source

Given a ray, the source of the reversed ray is the source of the ray.

@[simp]

theorem EuclidGeom.Ray.rev_rev_eq_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} : ray.reverse.reverse = ray

Reversing a ray twice gives back to the original ray.

@[simp]

theorem EuclidGeom.Seg.rev_rev_eq_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : seg.reverse.reverse = seg

Reversing a segment twice gives back to the original segment.

@[simp]

theorem EuclidGeom.SegND.rev_rev_eq_self {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.SegND.reverse (EuclidGeom.SegND.reverse seg_nd) = seg_nd

Reversing a nondegenerate segment twice gives back to the original nondegenerate segment.

@[simp]

theorem EuclidGeom.Ray.toDir_of_rev_eq_neg_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} : ray.reverse.toDir = -ray.toDir

Given a ray, the direction of the reversed ray is the negative of the direction of the ray.

theorem EuclidGeom.Ray.unitVecND_of_rev_eq_neg_unitVecND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} : ray.reverse.toDir.unitVecND = -ray.toDir.unitVecND

Given a ray, the direction vector of the reversed ray is the negative of the direction vector of the ray.

theorem EuclidGeom.Ray.unitVec_of_rev_eq_neg_unitVec {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} : ray.reverse.toDir.unitVec = -ray.toDir.unitVec

Given a ray, the direction vector of the reversed ray is the negative of the direction vector of the ray.

@[simp]

theorem EuclidGeom.Ray.toProj_of_rev_eq_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} : ray.reverse.toProj = ray.toProj

Given a ray, the projective direction of the reversed ray is the same as that of the ray.

@[simp]

theorem EuclidGeom.Seg.toVec_of_rev_eq_neg_toVec {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : seg.reverse.toVec = -seg.toVec

Given a segment, the vector associated to the reversed segment is the negative of the vector associated to the segment.

@[simp]

theorem EuclidGeom.SegND.toVecND_of_rev_eq_neg_toVecND {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : (EuclidGeom.SegND.reverse seg_nd).toVecND = -seg_nd.toVecND

Given a nondegenerate segment, the nondegenerate vector associated to the reversed nondegenerate segment is the negative of the nondegenerate vector associated to the nondegenerate segment.

@[simp]

theorem EuclidGeom.SegND.toDir_of_rev_eq_neg_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : (EuclidGeom.SegND.reverse seg_nd).toDir = -seg_nd.toDir

Given a nondegenerate segment, the direction of the reversed nondegenerate segment is the negative direction of the nondegenerate segment.

@[simp]

theorem EuclidGeom.SegND.toProj_of_rev_eq_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : (EuclidGeom.SegND.reverse seg_nd).toProj = seg_nd.toProj

Given a nondegenerate segment, the projective direction of the reversed nondegenerate segment is the same projective direction of the nondegenerate segment.

theorem EuclidGeom.Ray.source_lies_on_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} : EuclidGeom.lies_on ray.source ray.reverse

The source of a ray lies on the reverse of the ray.

theorem EuclidGeom.Seg.source_lies_on_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : EuclidGeom.lies_on seg.source seg.reverse

The source of a segment lies on the reverse of the segment.

theorem EuclidGeom.Seg.target_lies_on_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : EuclidGeom.lies_on seg.target seg.reverse

The target of a segment lies on the reverse of the segment.

theorem EuclidGeom.SegND.source_lies_on_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_on seg_nd.source (EuclidGeom.SegND.reverse seg_nd)

The source of a nondegenerate segment lies on the reverse of the segment.

theorem EuclidGeom.SegND.target_lies_on_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_on seg_nd.target (EuclidGeom.SegND.reverse seg_nd)

The target of a nondegenerate segment lies on the reverse of the segment.

theorem EuclidGeom.Ray.lies_on_rev_or_lies_on_iff {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {ray : EuclidGeom.Ray P} : EuclidGeom.lies_on X ray ∨ EuclidGeom.lies_on X ray.reverse ↔ EuclidGeom.lies_on X ray.reverse ∨ EuclidGeom.lies_on X ray.reverse.reverse

Given a ray, a point $X$ lies on the ray or its reverse if and only if $X$ lies on the reverse ray or the reverse of reverse ray.

theorem EuclidGeom.Seg.lies_on_rev_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg : EuclidGeom.Seg P} : EuclidGeom.lies_on A seg → EuclidGeom.lies_on A seg.reverse

If a point lies on a segment, then it lies on the reversed segment.

@[simp]

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

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

@[simp]

theorem EuclidGeom.Seg.lies_int_rev_iff_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg : EuclidGeom.Seg P} : EuclidGeom.lies_int A seg.reverse ↔ EuclidGeom.lies_int A seg

A point lies in the interior of the reverse of a segment if and only if it lies in the interior of the segment.

@[simp]

theorem EuclidGeom.SegND.lies_on_rev_iff_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_on A (EuclidGeom.SegND.reverse seg_nd) ↔ EuclidGeom.lies_on A seg_nd

Given a nondegenerate segment, a point lies on the reverse of the segment if and only if it lies on the segment.

@[simp]

theorem EuclidGeom.SegND.lies_int_rev_iff_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_int A (EuclidGeom.SegND.reverse seg_nd) ↔ EuclidGeom.lies_int A seg_nd

Given a nondegenerate segment, a point lies in the interior of the reverse of the segment if and only if it lies in the interior of the segment.

theorem EuclidGeom.pt_lies_on_ray_rev_iff_vec_opposite_dir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {ray : EuclidGeom.Ray P} : EuclidGeom.lies_on A ray.reverse ↔ ∃ t ≤ 0, EuclidGeom.Vec.mkPtPt ray.source A = t • ray.toDir.unitVec

Given a ray, a point $A$ lies on the reverse of the ray if and only if there exists a nonpositive real number $t$ such that the vector from the source of the ray to $A$ is $t$ times the direction vector of the ray.

theorem EuclidGeom.pt_lies_on_line_from_ray_iff_vec_parallel {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {ray : EuclidGeom.Ray P} : EuclidGeom.lies_on A ray ∨ EuclidGeom.lies_on A ray.reverse ↔ ∃ (t : ℝ), EuclidGeom.Vec.mkPtPt ray.source A = t • ray.toDir.unitVec

A point $A$ lies on the lines determined by a ray $ray$ (i.e. lies on the ray or its reverse) if and only if the vector from the source of ray to $A$ is a real multiple of the direction vector of $ray$.

theorem EuclidGeom.Ray.eq_source_iff_lies_on_and_lies_on_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {ray : EuclidGeom.Ray P} : A = ray.source ↔ EuclidGeom.lies_on A ray ∧ EuclidGeom.lies_on A ray.reverse

A point is equal to the source of a ray if and only if it lies on the ray and it lies on the reverse of the ray.

theorem EuclidGeom.Ray.not_lies_on_of_lies_int_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {ray : EuclidGeom.Ray P} (liesint : EuclidGeom.lies_int A ray.reverse) : ¬EuclidGeom.lies_on A ray

If a point lies in the interior of the reverse of a ray, then it does not lie on the ray.

theorem EuclidGeom.Ray.not_lies_int_of_lies_on_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {ray : EuclidGeom.Ray P} (liesint : EuclidGeom.lies_on A ray.reverse) : ¬EuclidGeom.lies_int A ray

If a point lies on of the reverse of a ray, then it does not lie in the interior of the ray.

theorem EuclidGeom.lies_on_iff_lies_on_toRay_and_rev_toRay {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_on X ↑seg_nd ↔ EuclidGeom.lies_on X seg_nd.toRay ∧ EuclidGeom.lies_on X (EuclidGeom.SegND.reverse seg_nd).toRay

A point lies on a nondegenerate segment $AB$ if and only if it lies on the ray $AB$ and on the reverse ray $BA$.

theorem EuclidGeom.lies_on_pt_toDir_of_pt_lies_on_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ray : EuclidGeom.Ray P} (hA : EuclidGeom.lies_on A ray) (hB : EuclidGeom.lies_on B ray.reverse) : EuclidGeom.lies_on A { source := B, toDir := ray.toDir }

Let $ray$ be a ray, and let $A$ be a point on $ray$, and $B$ a point on the reverse of $ray$. Then $A$ lies on the ray starting at $B$ in the same direction of $\ray$.

theorem EuclidGeom.lies_on_iff_lies_on_rev_of_same_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray₁ : EuclidGeom.Ray P} {ray₂ : EuclidGeom.Ray P} (h : ray₁.toDir = ray₂.toDir) : EuclidGeom.lies_on ray₁.source ray₂ ↔ EuclidGeom.lies_on ray₂.source ray₁.reverse

Given two rays $ray_1$ and $ray_2$ in same direction, the source of $ray_1$ lies on $ray_2$ if and only if the source of $ray_2$ lies on the reverse of $ray_1$.

theorem EuclidGeom.lies_int_iff_lies_int_rev_of_same_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray₁ : EuclidGeom.Ray P} {ray₂ : EuclidGeom.Ray P} (h : ray₁.toDir = ray₂.toDir) : EuclidGeom.lies_int ray₁.source ray₂ ↔ EuclidGeom.lies_int ray₂.source ray₁.reverse

Given two rays $ray_1$ and $ray_2$ in same direction, the source of $ray_1$ lies in the interior of $ray_2$ if and only if the source of $ray_2$ lies in the interior of the reverse of $ray_1$.

theorem EuclidGeom.lies_on_iff_lies_on_of_neg_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray₁ : EuclidGeom.Ray P} {ray₂ : EuclidGeom.Ray P} (h : ray₁.toDir = -ray₂.toDir) : EuclidGeom.lies_on ray₁.source ray₂ ↔ EuclidGeom.lies_on ray₂.source ray₁

Given two rays $ray_1$ and $ray_2$ in the opposite direction, the source of $ray_1$ lies on $ray_2$ if and only if the source of $ray_2$ lies on $ray_1$.

theorem EuclidGeom.lies_int_iff_lies_int_of_neg_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray₁ : EuclidGeom.Ray P} {ray₂ : EuclidGeom.Ray P} (h : ray₁.toDir = -ray₂.toDir) : EuclidGeom.lies_int ray₁.source ray₂ ↔ EuclidGeom.lies_int ray₂.source ray₁

Given two rays $ray_1$ and $ray_2$ in the opposite direction, the source of $ray_1$ lies in the interior of $ray_2$ if and only if the source of $ray_2$ lies in the interior of $ray_1$.

theorem EuclidGeom.lies_on_rev_iff_lies_on_rev_of_neg_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray₁ : EuclidGeom.Ray P} {ray₂ : EuclidGeom.Ray P} (h : ray₁.toDir = -ray₂.toDir) : EuclidGeom.lies_on ray₁.source ray₂.reverse ↔ EuclidGeom.lies_on ray₂.source ray₁.reverse

Given two rays $ray_1$ and $ray_2$ in the opposite direction, the source of $ray_1$ lies on the reverse of $ray_2$ if and only if the source of $ray_2$ lies on the reverse of $ray_1$.

theorem EuclidGeom.lies_int_rev_iff_lies_int_rev_of_neg_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray₁ : EuclidGeom.Ray P} {ray₂ : EuclidGeom.Ray P} (h : ray₁.toDir = -ray₂.toDir) : EuclidGeom.lies_int ray₁.source ray₂.reverse ↔ EuclidGeom.lies_int ray₂.source ray₁.reverse

Given two rays $ray_1$ and $ray_2$ in the opposite direction, the source of $ray_1$ lies in the interior of the reverse of $ray_2$ if and only if the source of $ray_2$ lies in the interior of the reverse of $ray_1$.

theorem EuclidGeom.lies_on_or_rev_iff_exist_real_vec_eq_smul {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {ray : EuclidGeom.Ray P} : EuclidGeom.lies_on A ray ∨ EuclidGeom.lies_on A ray.reverse ↔ ∃ (t : ℝ), EuclidGeom.Vec.mkPtPt ray.source A = t • ↑ray.toDir.unitVecND

Given a ray, a point $A$ lies on the ray or its reverse ray if and only if there exists a real number $t$ such that the vector from the source of the ray to $A$ is $t$ times the direction of the ray.

theorem EuclidGeom.ray_toProj_eq_mk_pt_pt_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} {ray : EuclidGeom.Ray P} [h : EuclidGeom.PtNe B A] (ha : EuclidGeom.lies_on A ray ∨ EuclidGeom.lies_on A ray.reverse) (hb : EuclidGeom.lies_on B ray ∨ EuclidGeom.lies_on B ray.reverse) : ray.toProj = (RAY A B).toProj

Given two distinct points $A$ and $B$ and a ray, if both $A$ and $B$ lies on the ray or its reversed ray, then the projective direction of the ray is the same as the projective direction of the ray $AB$.

theorem EuclidGeom.SegND.pt_target_toDir_eq_toDir_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} {A : P} (h : EuclidGeom.lies_int A seg_nd) : (SEG_nd A seg_nd.target (_ : (↑seg_nd).target ≠ A)).toDir = seg_nd.toDir

Given a nondegenerate segment $Segnd$ and a point $A$ lies in the interior of it. Then the direction of the nondegenerate segment from $A$ to the target of $Segnd$ equals the direction of $Segnd$.

theorem EuclidGeom.SegND.toDir_eq_neg_toDir_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (h : EuclidGeom.lies_int A seg_nd) : (VEC_nd A seg_nd.source (_ : (↑seg_nd).source ≠ A)).toDir = -(VEC_nd A seg_nd.target (_ : (↑seg_nd).target ≠ A)).toDir

Given a nondegenerate segment $Segnd$ and a point $A$ lies in the interior of it. Then the direction of the nondegenerate vector from $A$ to the source of $Segnd$ equals the opposite direction of the nondegenerate vector from $A$ to the target of $Segnd$.

theorem EuclidGeom.SegND.toDir_eq_neg_toDir_of_lies_int' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (h : EuclidGeom.lies_int A seg_nd) : (VEC_nd seg_nd.source A (_ : A ≠ (↑seg_nd).source)).toDir = -(VEC_nd seg_nd.target A (_ : A ≠ (↑seg_nd).target)).toDir

Given a nondegenerate segment $Segnd$ and a point $A$ lies in the interior of it. Then the direction of the nondegenerate vector from the source of $Segnd$ to $A$ equals the opposite direction of the nondegenerate vector from the target of $Segnd$ to $A$.

theorem EuclidGeom.Ray.lies_int_rev_iff_neg_of_vec_eq_smul_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {ray : EuclidGeom.Ray P} {A : P} {t : ℝ} (h : EuclidGeom.Vec.mkPtPt ray.source A = t • ray.toDir.unitVec) : EuclidGeom.lies_int A ray.reverse ↔ t < 0

(7) Extension

def EuclidGeom.SegND.extension {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg_nd : EuclidGeom.SegND P) : EuclidGeom.Ray P

Define the extension ray of a nondegenerate segment to be the ray whose origin is the target of the segment whose direction is the same as that of the segment.

Equations

• EuclidGeom.SegND.extension seg_nd = { source := seg_nd.target, toDir := seg_nd.toDir }

theorem EuclidGeom.SegND.extn_eq_rev_toRay_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.SegND.extension seg_nd = (EuclidGeom.SegND.reverse seg_nd).reverse

The extension of a nondegenerate segment is the same as first reverse the segment, then take the ray associated to the segment, and finally reverse the ray.

theorem EuclidGeom.SegND.rev_extn_eq_toRay_rev {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.SegND.extension (EuclidGeom.SegND.reverse seg_nd) = seg_nd.reverse

The extension of the reverse of a nondegenerate segment is the same as the reverse of the ray associated to the segment.

@[simp]

theorem EuclidGeom.SegND.extn_toDir {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : (EuclidGeom.SegND.extension seg_nd).toDir = seg_nd.toDir

The direction of the extension ray of a nondegenerate segment is the same as the direction of the segment.

@[simp]

theorem EuclidGeom.SegND.extn_toProj {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : (EuclidGeom.SegND.extension seg_nd).toProj = seg_nd.toProj

The projective direction of the extension ray of a nondegenerate segment is the same as the projective direction of the segment.

theorem EuclidGeom.SegND.eq_target_iff_lies_on_lies_on_extn {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_on A seg_nd ∧ EuclidGeom.lies_on A (EuclidGeom.SegND.extension seg_nd) ↔ A = seg_nd.target

Given a nondegenerate segment, a point is equal to its target if and only if it lies on the segment and its extension ray.

theorem EuclidGeom.SegND.target_lies_int_seg_source_pt_of_pt_lies_int_extn {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} (liesint : EuclidGeom.lies_int X (EuclidGeom.SegND.extension seg_nd)) : EuclidGeom.lies_int seg_nd.target { source := seg_nd.source, target := X }

Given a nondegenerate segment $AB$, if a point $X$ belongs to the interior of the extension ray of $AB$, then $B$ lies in the interior of $AX$.

theorem EuclidGeom.SegND.lies_on_seg_nd_or_extension_of_lies_on_toRay {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} {A : P} (h : EuclidGeom.lies_on A seg_nd.toRay) : EuclidGeom.lies_on A seg_nd ∨ EuclidGeom.lies_on A (EuclidGeom.SegND.extension seg_nd)

If a point lies on the ray associated to a segment, then either it lies on the segment or it lies on the extension ray of the segment.

theorem EuclidGeom.SegND.lies_int_toRay_of_lies_on_extn {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} (A : P) (h : EuclidGeom.lies_on A (EuclidGeom.SegND.extension seg_nd)) : EuclidGeom.lies_int A seg_nd.toRay

If a point lies on the extension ray associated to a nondegenerate segment, then it lies on the interior of the ray associated to the segment

theorem EuclidGeom.SegND.not_lies_int_rev_extn_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (lieson : EuclidGeom.lies_on A ↑seg_nd) : ¬EuclidGeom.lies_int A (EuclidGeom.SegND.extension (EuclidGeom.SegND.reverse seg_nd))

theorem EuclidGeom.SegND.not_lies_int_extn_of_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (lieson : EuclidGeom.lies_on A ↑seg_nd) : ¬EuclidGeom.lies_int A (EuclidGeom.SegND.extension seg_nd)

def EuclidGeom.Ray.extpoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.Ray P) (t : ℝ) : P

Equations

• EuclidGeom.Ray.extpoint l t = t • l.toDir.unitVec +ᵥ l.source

theorem EuclidGeom.Ray.extpoint_lies_on_of_nonneg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {t : ℝ} (ht : 0 ≤ t) : EuclidGeom.lies_on (EuclidGeom.Ray.extpoint r t) r

theorem EuclidGeom.Ray.lies_on_of_eq_nonneg_extpoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {A : P} {t : ℝ} (ht : 0 ≤ t) (h : A = EuclidGeom.Ray.extpoint r t) : EuclidGeom.lies_on A r

theorem EuclidGeom.Ray.extpoint_lies_int_of_pos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {t : ℝ} (ht : 0 < t) : EuclidGeom.lies_int (EuclidGeom.Ray.extpoint r t) r

theorem EuclidGeom.Ray.lies_int_of_eq_pos_extpoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {A : P} {t : ℝ} (ht : 0 < t) (h : A = EuclidGeom.Ray.extpoint r t) : EuclidGeom.lies_int A r

theorem EuclidGeom.Ray.dist_of_extpoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {t : ℝ} (ht : 0 ≤ t) : dist r.source (EuclidGeom.Ray.extpoint r t) = t

theorem EuclidGeom.Ray.dist_eq_of_eq_extpoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] {r : EuclidGeom.Ray P} {A : P} {t : ℝ} (ht : 0 ≤ t) (h : A = EuclidGeom.Ray.extpoint r t) : dist r.source A = t

(8) Length

def EuclidGeom.Seg.length {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg : EuclidGeom.Seg P) : ℝ

This function gives the length of a given segment, which is the distance between the source and target of the segment.

Equations

• seg.length = dist seg.source seg.target

@[simp]

theorem EuclidGeom.Seg.length_eq_dist {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} : { source := A, target := B }.length = dist A B

The length of segment $AB$ is the same as the distance form $A$ to $B$.

theorem EuclidGeom.Seg.length_eq_norm_toVec {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : seg.length = ‖seg.toVec‖

The length of a given segment is the same as the norm of the vector associated to the segment.

@[inline, reducible]

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

This function defines the length of a nondegenerate segment, which is just the length of the segment.

Equations

• EuclidGeom.SegND.length seg_nd = (↑seg_nd).length

theorem EuclidGeom.Seg.length_nonneg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : 0 ≤ seg.length

Every segment has nonnegative length.

theorem EuclidGeom.Seg.length_pos_iff_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : 0 < seg.length ↔ EuclidGeom.Seg.IsND seg

A segment has positive length if and only if it is nondegenerate.

theorem EuclidGeom.Seg.length_ne_zero_iff_nd {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : 0 ≠ seg.length ↔ EuclidGeom.Seg.IsND seg

The length of a given segment is nonzero if and only if the segment is nondegenerate.

theorem EuclidGeom.SegND.length_pos {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : 0 < EuclidGeom.SegND.length seg_nd

A nondegenerate segment has strictly positive length.

theorem EuclidGeom.Seg.length_sq_eq_inner_toVec_toVec {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : seg.length ^ 2 = inner seg.toVec seg.toVec

Given a segment, the square of its length is equal to the the inner product of the associated vector with itself.

theorem EuclidGeom.Seg.length_eq_zero_iff_deg {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : seg.length = 0 ↔ seg.target = seg.source

The length of a segment is zero if and only if it is degenerate, i.e. it has same source and target.

@[simp]

theorem EuclidGeom.Seg.length_of_rev_eq_length {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : seg.reverse.length = seg.length

Reversing a segment does not change its length.

@[simp]

theorem EuclidGeom.SegND.length_of_rev_eq_length {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.SegND.length (EuclidGeom.SegND.reverse seg_nd) = EuclidGeom.SegND.length seg_nd

Reversing a segment does not change its length.

theorem EuclidGeom.length_of_rev_eq_length' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {B : P} : { source := B, target := A }.length = { source := A, target := B }.length

The length of segment $AB$ is the same as the length of segment $BA$.

theorem EuclidGeom.length_eq_length_add_length {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} {A : P} (lieson : EuclidGeom.lies_on A seg) : seg.length = { source := seg.source, target := A }.length + { source := A, target := seg.target }.length

Given a segment and a point that lies on the segment, the additional point will separate the segment into two segments, whose lengths add up to the length of the original segment.

theorem EuclidGeom.SegND.length_eq_length_add_length_of_lies_on_extn {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} {A : P} (h : EuclidGeom.lies_on A (EuclidGeom.SegND.extension seg_nd)) : { source := seg_nd.source, target := A }.length = (↑seg_nd).length + { source := seg_nd.target, target := A }.length

theorem EuclidGeom.Seg.dist_lt_length_of_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {s : EuclidGeom.Seg P} {A : P} (h : EuclidGeom.lies_int A s) : dist s.source A < s.length

(9) Midpoint

def EuclidGeom.Seg.midpoint {P : Type u_1} [EuclidGeom.EuclideanPlane P] (seg : EuclidGeom.Seg P) : P

Given a segment $AB$, this function returns the midpoint of $AB$, defined as moving from $A$ by the vector $\overrightarrow{AB}/2$.

Equations

• seg.midpoint = (1 / 2) • seg.toVec +ᵥ seg.source

@[inline, reducible]

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

Equations

• EuclidGeom.SegND.midpoint seg_nd = (↑seg_nd).midpoint

theorem EuclidGeom.Seg.vec_source_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : EuclidGeom.Vec.mkPtPt seg.source seg.midpoint = (1 / 2) • EuclidGeom.Vec.mkPtPt seg.source seg.target

theorem EuclidGeom.SegND.vec_source_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.Vec.mkPtPt seg_nd.source (EuclidGeom.SegND.midpoint seg_nd) = (1 / 2) • EuclidGeom.Vec.mkPtPt seg_nd.source seg_nd.target

Given a segment $AB$, the vector from the midpoint of $AB$ to $B$ is half of the vector from $A$ to $B$

theorem EuclidGeom.Seg.vec_midpt_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : EuclidGeom.Vec.mkPtPt seg.midpoint seg.target = (1 / 2) • EuclidGeom.Vec.mkPtPt seg.source seg.target

theorem EuclidGeom.SegND.vec_midpt_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.Vec.mkPtPt (EuclidGeom.SegND.midpoint seg_nd) seg_nd.target = (1 / 2) • EuclidGeom.Vec.mkPtPt seg_nd.source seg_nd.target

theorem EuclidGeom.Seg.vec_midpt_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : EuclidGeom.Vec.mkPtPt seg.source seg.midpoint = EuclidGeom.Vec.mkPtPt seg.midpoint seg.target

Given a segment $AB$, the vector from $A$ to the midpoint of $AB$ is same as the vector from the midpoint of $AB$ to $B$

theorem EuclidGeom.SegND.vec_midpt_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.Vec.mkPtPt seg_nd.source (EuclidGeom.SegND.midpoint seg_nd) = EuclidGeom.Vec.mkPtPt (EuclidGeom.SegND.midpoint seg_nd) seg_nd.target

theorem EuclidGeom.Seg.vec_eq_of_eq_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg : EuclidGeom.Seg P} (h : X = seg.midpoint) : EuclidGeom.Vec.mkPtPt seg.source X = EuclidGeom.Vec.mkPtPt X seg.target

Given a segment $AB$ and its midpoint P, the vector from $A$ to $P$ is same as the vector from $P$ to $B$

theorem EuclidGeom.SegND.vec_eq_of_eq_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (h : A = EuclidGeom.SegND.midpoint seg_nd) : EuclidGeom.Vec.mkPtPt seg_nd.source A = EuclidGeom.Vec.mkPtPt A seg_nd.target

theorem EuclidGeom.Seg.midpt_of_vector_from_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg : EuclidGeom.Seg P} (h : EuclidGeom.Vec.mkPtPt seg.source A = (1 / 2) • EuclidGeom.Vec.mkPtPt seg.source seg.target) : A = seg.midpoint

Given a segment $AB$ and a point P, if vector $\overrightarrow{AP}$ is half of vector $\overrightarrow{AB}$, P is the midpoint of $AB$.

theorem EuclidGeom.SegND.midpt_of_vector_from_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (h : EuclidGeom.Vec.mkPtPt seg_nd.source A = (1 / 2) • EuclidGeom.Vec.mkPtPt seg_nd.source seg_nd.target) : A = EuclidGeom.SegND.midpoint seg_nd

theorem EuclidGeom.Seg.midpt_of_vector_to_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg : EuclidGeom.Seg P} (h : EuclidGeom.Vec.mkPtPt A seg.target = (1 / 2) • EuclidGeom.Vec.mkPtPt seg.source seg.target) : A = seg.midpoint

Given a segment $AB$ and a point P, if vector $\overrightarrow{PB}$ is half of vector $\overrightarrow{AB}$, P is the midpoint of $AB$.

theorem EuclidGeom.SegND.midpt_of_vector_to_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (h : EuclidGeom.Vec.mkPtPt A seg_nd.target = (1 / 2) • EuclidGeom.Vec.mkPtPt seg_nd.source seg_nd.target) : A = EuclidGeom.SegND.midpoint seg_nd

theorem EuclidGeom.Seg.midpt_of_same_vector_to_source_and_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg : EuclidGeom.Seg P} (h : EuclidGeom.Vec.mkPtPt seg.source A = EuclidGeom.Vec.mkPtPt A seg.target) : A = seg.midpoint

Given a segment $AB$ and a point P, if vector $\overrightarrow{AP}$ is same as vector $\overrightarrow{PB}$, P is the midpoint of $AB$.

theorem EuclidGeom.SegND.midpt_of_same_vector_to_source_and_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (h : EuclidGeom.Vec.mkPtPt seg_nd.source A = EuclidGeom.Vec.mkPtPt A seg_nd.target) : A = EuclidGeom.SegND.midpoint seg_nd

theorem EuclidGeom.Seg.midpt_lies_on {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : EuclidGeom.lies_on seg.midpoint seg

The midpoint of a segment lies on the segment.

theorem EuclidGeom.Seg.lies_on_of_eq_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg : EuclidGeom.Seg P} (h : A = seg.midpoint) : EuclidGeom.lies_on A seg

The midpoint of a segment lies on the segment.

theorem EuclidGeom.SegND.midpt_lies_int {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_int (EuclidGeom.SegND.midpoint seg_nd) seg_nd

The midpoint of a nondegenerate segment lies in the interior of the segment.

theorem EuclidGeom.SegND.midpt_ne_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.SegND.midpoint seg_nd ≠ seg_nd.source

The midpoint of a nondegenerate segment is not equal to the source of the segment.

theorem EuclidGeom.SegND.midpt_ne_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.SegND.midpoint seg_nd ≠ seg_nd.target

The midpoint of a nondegenerate segment is not equal to the target of the segment.

theorem EuclidGeom.SegND.lies_int_of_eq_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {A : P} {seg_nd : EuclidGeom.SegND P} (h : A = EuclidGeom.SegND.midpoint seg_nd) : EuclidGeom.lies_int A seg_nd

The midpoint of a nondegenerate segment lies in the interior of the segment.

theorem EuclidGeom.Seg.midpt_iff_same_vector_to_source_and_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg : EuclidGeom.Seg P} : X = seg.midpoint ↔ { source := seg.source, target := X }.toVec = { source := X, target := seg.target }.toVec

A point $X$ on a given segment $AB$ is the midpoint if and only if the vector $\overrightarrow{AX}$ is the same as the vector $\overrightarrow{XB}$.

theorem EuclidGeom.SegND.midpt_iff_same_vector_to_source_and_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} : X = EuclidGeom.SegND.midpoint seg_nd ↔ { source := seg_nd.source, target := X }.toVec = { source := X, target := seg_nd.target }.toVec

theorem EuclidGeom.Seg.dist_target_eq_dist_source_of_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : { source := seg.source, target := seg.midpoint }.length = { source := seg.midpoint, target := seg.target }.length

The midpoint of a segment has same distance to the source and to the target of the segment.

theorem EuclidGeom.Seg.dist_target_eq_dist_source_of_midpt' {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : { source := seg.midpoint, target := seg.source }.length = { source := seg.midpoint, target := seg.target }.length

The midpoint of a segment has same distance to the source and to the target of the segment.

theorem EuclidGeom.Seg.two_nsmul_dist_midpt_source_eq_length {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : 2 • dist seg.midpoint seg.source = seg.length

theorem EuclidGeom.Seg.two_nsmul_dist_midpt_target_eq_length {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : 2 • dist seg.midpoint seg.target = seg.length

theorem EuclidGeom.Seg.dist_target_eq_dist_source_of_eq_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg : EuclidGeom.Seg P} (h : X = seg.midpoint) : { source := seg.source, target := X }.length = { source := X, target := seg.target }.length

The midpoint of a segment has same distance to the source and to the target of the segment.

theorem EuclidGeom.Seg.eq_midpt_iff_in_seg_and_dist_target_eq_dist_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg : EuclidGeom.Seg P} : X = seg.midpoint ↔ EuclidGeom.lies_on X seg ∧ { source := seg.source, target := X }.length = { source := X, target := seg.target }.length

A point $X$ is the midpoint of a segment $AB$ if and only if $X$ lies on $AB$ and $X$ has equal distance to $A$ and $B$.

theorem EuclidGeom.SegND.eq_midpt_iff_in_seg_and_dist_target_eq_dist_source {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg_nd : EuclidGeom.SegND P} : X = EuclidGeom.SegND.midpoint seg_nd ↔ EuclidGeom.lies_on X seg_nd ∧ { source := seg_nd.source, target := X }.length = { source := X, target := seg_nd.target }.length

theorem EuclidGeom.Seg.reverse_midpt_eq_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : seg.reverse.midpoint = seg.midpoint

theorem EuclidGeom.SegND.reverse_midpt_eq_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.SegND.midpoint (EuclidGeom.SegND.reverse seg_nd) = EuclidGeom.SegND.midpoint seg_nd

(10) Existence theorem

theorem EuclidGeom.Seg.target_eq_vec_vadd_target_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : seg.target = { source := seg.source, target := seg.toVec +ᵥ seg.target }.midpoint

Given a segment $AB$, the midpoint of $A$ and $B + \overrightarrow{AB}$ is B.

theorem EuclidGeom.SegND.target_eq_vec_vadd_target_midpt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : seg_nd.target = { source := seg_nd.source, target := ↑seg_nd.toVecND +ᵥ seg_nd.target }.midpoint

theorem EuclidGeom.SegND.target_lies_int_seg_source_vec_vadd_target {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : EuclidGeom.lies_int seg_nd.target { source := seg_nd.source, target := ↑seg_nd.toVecND +ᵥ seg_nd.target }

This theorem should be replaced! B is midpt of A and B + VEC A B, midpt liesint a seg_nd Given a nondegenerate segment $AB$, B lies in the interior of the segment of $A(B + \overrightarrow{AB})$.

theorem EuclidGeom.SegND.exist_pt_beyond_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] (l : EuclidGeom.SegND P) : ∃ (q : P), EuclidGeom.lies_int l.target { source := l.source, target := q }

Archimedean property I : given a directed segment AB (with A ≠ B), then there exists a point P such that B lies on the directed segment AP and P ≠ B.

theorem EuclidGeom.Seg.nd_of_exist_int_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {X : P} {seg : EuclidGeom.Seg P} (h : EuclidGeom.lies_int X seg) : EuclidGeom.Seg.IsND seg

Archimedean property II: On an nontrivial directed segment, one can always find a point in its interior. This will be moved to later disccusion about midpoint of a segment, as the midpoint is a point in the interior of a nontrivial segment If a segment contains an interior point, then it is nondegenerate

theorem EuclidGeom.Seg.nd_iff_exist_int_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : (∃ (X : P), EuclidGeom.lies_int X seg) ↔ EuclidGeom.Seg.IsND seg

A segment is nondegenerate if and only if it contains an interior point.

theorem EuclidGeom.SegND.exist_int_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : ∃ (X : P), EuclidGeom.lies_int X seg_nd

If a segment is nondegenerate, it contains an interior point.

theorem EuclidGeom.Seg.length_pos_iff_exist_int_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg : EuclidGeom.Seg P} : 0 < seg.length ↔ ∃ (X : P), EuclidGeom.lies_int X seg

A segment contains an interior point if and only if its length is positive.

theorem EuclidGeom.SegND.length_pos_iff_exist_int_pt {P : Type u_1} [EuclidGeom.EuclideanPlane P] {seg_nd : EuclidGeom.SegND P} : 0 < EuclidGeom.SegND.length seg_nd ↔ ∃ (X : P), EuclidGeom.lies_int X seg_nd

theorem EuclidGeom.Ray.nontriv {P : Type u_1} [EuclidGeom.EuclideanPlane P] (ray : EuclidGeom.Ray P) : ∃ (A : P) (B : P), A ∈ EuclidGeom.Ray.carrier ray ∧ B ∈ EuclidGeom.Ray.carrier ray ∧ B ≠ A

A ray contains two distinct points.