In this file, we define the concept for two lines to be parallel. A more precise plan is the following:
We define a class called linear objects, consisting of one of the five types: nondegenerate vector, direction, ray, nondegenerate segment, and line.
We define the meaning of any pair of linear objects to be parallel.
We prove that coercion among linear objects generates linear objects that are parallel to the original ones.
We prove theorems related to that non-parallel lines intersection, and define the intersections.
Future Work #
Comments about LinearObj is outdated. Now we use ProjObj
Given two linear objects $l_1$ and $l_2$ (not necessarily of the same type), this function returns whether they are parallel, defined as having the same associated projective direction.
Equations
- EuclidGeom.Parallel l₁ l₂ = (EuclidGeom.toProj l₁ = EuclidGeom.toProj l₂)
Instances For
Being parallel defines an equivalence relation among all linear objects, that is they satisfy the three conditions: (1) reflexive: every linear object $l$ is parallel to itself; (2) symmetric: if the linear object $l_1$ is parallel to the linear object $l_2$, then $l_2$ is $l_1$; (3) transitive: if the linear object $l_1$ is parallel to the linear object $l_2$, and if the linear object $l_2$ is parallel to the linear object $l_3$, then $l_1$ is parallel to $l_3$.
This is to rewrite \verb|Parallel l l'| as \verb|l ParallelTo l'|
Equations
- One or more equations did not get rendered due to their size.
Instances For
This is to rewrite \verb|Parallel l l'| as $l \parallel l'$.
Equations
- EuclidGeom.«term_∥_» = Lean.ParserDescr.trailingNode `EuclidGeom.term_∥_ 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∥ ") (Lean.ParserDescr.cat `term 51))
Instances For
The projective direction of a ray is same as the projective direction of the extension line of the ray.
The projective direction of a nondegenerate segment is same as the projective direction of the extension line of it.
Given a nondegenate segment, it is parallel to the ray associated to this nondegenerate segment.
Given a nondegenerate segment, it is parallel to its associated directed line.
Given a nondegenate segment, it is parallel to the extension line of this nondegenerate segment.
Given a ray, the ray is parallel to the directed line associated to the ray.
Given a ray, the ray is parallel to the line associated to the ray.
A directed line is parallel to the line associated to the directed line.
If two nondegenerate segements are parallel, then their associated rays are parallel.
If the associated rays of two nondegenerate segments are parallel, then the two segments are parallel.
Given two nondegenerate segments, they are parallel if and only if their associated rays are parallel.
If two nondegenerate segments are not parallel, then their associated rays are not parallel.
If the associated rays of two nondegenerate segments are not parallel, then the two segments are not parallel.
Given two nondegenerate segments, they are not parallel if and only if their associated rays are not parallel.
If two nondegenerate segments are parallel, then their associated directed lines are parallel.
If two nondegenerate segments have parallel directed lines, then the segments themselves are parallel.
Given two nondegenerate segments, their associated direction lines are parallel if and only if the segments are parallel.
If two nondegenerate segments are not parallel, then their associated directed lines are not parallel.
If the associated directed lines of two nondegenerate segments are not parallel, then the two segments are not parallel.
Given two nondegenerate segments, they are not parallel if and only if their associated directed lines are not parallel.
If two nondegenerate segments are parallel, then their associated lines are parallel.
If the lines associated to two nondegenerate segments are parallel, then the two segments are parallel.
The nondegenerate segments $s$ and $s'$ are parallel if and only if their associated lines are parallel.
Given two nondegenerate segments, if they are not parallel, then their associated lines are not parallel.
Given two nondegenerate segments, their asscociated lines are not parallel if and only if they are not parallel.
This theorem states that two nondegenerate segments are not parallel if and only if their associated lines are not parallel.
If the directed lines associated to two rays are parallel, then the two rays are parallel.
This theorem states that two rays are parallel if and only if their associated direction lines are parallel.
If two rays are not parallel, then their associated directed lines are not parallel.
If the directed lines associated to two rays are not parallel, then the two rays are not parallel.
If two rays are not parallel, then their associated directed lines are not parallel.
Given two parallel rays, their extension lines are parallel.
If the lines associated to two rays are parallel, then thew two rays are parallel.
The extension lines of two rays are parallel if and only if the rays themselves are parallel.
Given two rays, if their extension lines are not parallel, they are not parallel.
If two rays have non-parallel associated lines, then the rays themselves are not parallel.
This theorem states that two rays are not parallel if and only if their associated lines are not parallel.
If two directed lines are parallel, then their associated lines are also parallel.
Given two directed lines $l_1$ and $l_2$, if their associated lines are parallel, then the two directed lines are parallel.
Given two directed lines $l_1$ and $l_2$, $l_1$ is parallel to $l_2$ if and only if the underlying lines of $l_1$ and $l_2$ are parallel.
The non-parallelism of two direction lines $l_1$ and $l_2$ is equivalent to the non-parallelism of their associated lines.
Given two directed lines l₁ and l₂, if they are not parallel, then their associated lines are not parallel.
Given two directed lines l₁ and l₂, if their associated lines are not parallel, then the two directed lines are not parallel.
For two parallel directed figures $l_1$ and $l_2$, $l_1$ is parallel to the reverse of $l_2$.
Given two nondegenerate segments, if they are parallel, then the reverse of the second segment is parallel to the first segment.
If two rays are parallel, then one ray is parallel to the reverse of the other ray.
Given two parallel directed lines $l_1$ and $l_2$, $l_1$ is parallel to the reverse of $l_2$.
For two directed figures $l_1$ and $l_2$, if they are not parallel, then $l_1$ is not parallel to the reverse of $l_2$.
If two nondegenerate segments $s$ and $s'$ are not parallel, then $s$ is not parallel to the reverse of $s'$.
Given two rays, if their extension lines are not parallel, they are not parallel.
If two directed lines $l$ and $l'$ are not parallel, then $l$ is not parallel to the reverse of $l'$.
If $l_1$ and $l_2$ are two parallel directed figure, then the reverse of $l_1$ is parallel to $l_2$.
Given two nondegenerate segments $s$ and $s'$, if they are parallel, then the reverse of $s$ is parallel to $s'$.
If two rays $r$ and $r'$ are parallel, then the reverse of $r$ is parallel to $r'$.
If two directed lines $l$ and $l'$ are parallel, then the reverse of $l$ is parallel to $l'$.
Given two directed figures $l_1$ and $l_2$, if they are not parallel, then the reverse of $l_1$ is not parallel to $l_2$.
Given two nondegenerate segments, if they are not parallel, then reverse of the first segment is not parallel to the second segment.
Given two rays $r$ and $r'$, if they are not parallel, then the reverse of $r$ is not parallel to $r'$.
Given two directed lines $l$ and $l'$, if they are not parallel, then the reverse of $l$ is not parallel to $l'$.
If two directed figures $l_1$ and $l_2$ are parallel, then the reverse of $l_1$ is parallel to the reverse of $l_2$.
AI Given two nondegenerate segments $s$ and $s'$, if they are parallel, then their reverses are parallel.
If two rays are parallel, then their reverse rays are also parallel.
If two directed lines $l_1$ and $l_2$ are parallel, then their reverses are parallel.
Given two unparallel directed figures, then their reverses are not parallel either.
Given two nondegenerate segments, if they are not parallel, then their reverses are not parallel.
Given two rays $r$ and $r'$, if they are not parallel, then their reverse rays are not parallel.
Given two unparallel lines, their reverses are not parallel.
Given two directed figures $l_1$ and $l_2$, $l_1$ is parallel to the reverse of $l_2$ if and only if $l_1$ is parallel to $l_2$.
Given two nondegenerate segments $s$ and $s'$, $s$ is parallel to the reverse of $s'$ if and only if $s$ is parallel to $s'$.
Given two rays $r$ and $r'$, $r$ is parallel to the reverse of $r'$ if and only if $r$ is parallel to $r'$.
Given two directed lines $l$ and $l'$, $l$ is parallel to the reverse of $l'$ if and only if $l$ and $l'$ are parallel.
For two directed figures $l_1$ and $l_2$, $l_1$ is not parallel to the reverse of $l_2$ if and only if $l_1$ is not parallel to $l_2$.
Given three vectors $\vec u$, $\vec v$ and $\vec w$, we may write $\vec w$ as a linear combination of $\vec u$ and $\vec v$ (usually), i.e. $\vec w = c_u \vec u + c_v \vec v$. This function returns $c_u$, which we call the \emph{first linear coefficients} later on. When $\vec u$ and $\vec v$ are linearly dependent, we return $0$.
Equations
- EuclidGeom.cu u v w = ((EuclidGeom.Vec.det u) v)⁻¹ * (EuclidGeom.Vec.det w) v
Instances For
Given three vectors $\vec u$, $\vec v$ and $\vec w$, we may write $\vec w$ as a linear combination of $\vec u$ and $\vec v$ (usually), i.e. $\vec w = c_u \vec u + c_v \vec v$. This function returns $c_v$, which we call the \emph{second linear coefficients} later on. When $\vec u$ and $\vec v$ are linearly dependent, we return $0$.
Equations
- EuclidGeom.cv u v w = ((EuclidGeom.Vec.det u) v)⁻¹ * (EuclidGeom.Vec.det u) w
Instances For
Given three vectors $\vec u$, $\vec v$ and $\vec w$, the first linear coefficients to write $\vec w$ in terms of $\vec u$ and $\vec v$ is the same as the second linear coefficients to write $\vec w$ in terms of $\vec v$ and $\vec u$, i.e. after reversing the two base vectors.
Given three vectors $\vec u$, $\vec v$, and $\vec w$, if we change $\vec w$ to $-\vec w$, then the first linear combination coefficients is negated.
Let $\vec u$, $\vec v$ and $\vec w$ be three vectors such that $\vec v$ is nonzero and $\vec u$ is not a multiple of $\vec v$, then $\vec w$ is the linear combination of $\vec u$ and $\vec v$ with the first and second linear coefficients respectively, i.e. $\vec w = c_u(\vec u, \vec v, \vec w) \cdot \vec u + c_v(\vec u, \vec v, \vec w) \cdot \vec v$.
Given two nondegenerate vectors $\vec u$ and $\vec v$ of distinct projective directions, any vector $w$ is the linear combination of $\vec u$ and $\vec v$ with coefficients, namely, $\vec w = c_u(\vec u, \vec v, \vec w) \vec u + c_v(\vec u, \vec v, \vec w) \vec v$.
Given two directions $\vec u$ and $\vec v$ of different projective directions, any vector $w$ is the linear combination of $\vec u$ and $\vec v$ with coefficients, namely, $\vec w = c_u(\vec u, \vec v, \vec w) \vec u + c_v(\vec u, \vec v, \vec w) \vec v$.
Given two unparallel rays, this function returns the intersection of their associated lines.
Equations
- EuclidGeom.inx_of_extn_line r₁ r₂ _h = EuclidGeom.cu (↑r₁.toDir.unitVecND) (↑r₂.toDir.unitVecND) (EuclidGeom.Vec.mkPtPt r₁.source r₂.source) • r₁.toDir.unitVec +ᵥ r₁.source
Instances For
Given two unparallel rays $r_1$ and $r_2$, the intersection of the lines of $r_1$ and $r_2$ is the same as the intersection of the lines of $r_2$ and $r_1$.
Given two unparallel rays $r_1$ and $r_2$, the point given by function "inx_of_extn_line" lies on the extension line of $r_1$
Given two unparallel rays $r_1$ and $r_2$, the point given by function "inx_of_extn_line" lies on the extension line of $r_2$
Given two rays $r_1$ and $r_2$, if they have the same projective direction and the source of $r_1$ lies on the extension line of $r_2$, then the two rays have same extension lines.
Let $a_1$, $a_2$, $b_1$, and $b_2$ be four rays such that $a_1$ and $a_2$ have the same extension line and $b_1$ and $b_2$ have the same extension line. If $a_1$ is not parallel to $b_1$ and $a_2$ is not parallel to $b_2$, then the intersection of extension lines of $a_1$ and $b_1$ is same as that of $a_2$ and $b_2$
Given two unparallel lines, this function returns the intersection point of these two lines.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given two unparallel line $l_1$ $l_2$, the point given by function "Line.inx" lies on $l_1$
Given two unparallel line $l_1$ $l_2$, the point given by function "Line.inx" lies on $l_2$
Given two unparallel line $l_1$ $l_2$, the point given by function "Line.inx" is exactly the intersection of these two lines
Two unparallel lines have only one intersection point, i.e. if two points $A$ and $B$ are both intersection points of unparallel lines $l_1$ and $l_2$, then $B = A$.
Given two unparallel line $l_1$ $l_2$, the point given by function "Line.inx" is exactly the intersection of these two lines
The symmetry of Line.inx, i.e. for two unparallel lines $l_1$ and $l_2$, the intersection of $l_1$ with $l_2$ is the same as the intersection of $l_2$ with $l_1$.
If two parallel lines share a same point, they are exactly the same line.
If two lines are not parallel, then their intersection is not empty, i.e. there exists a point that lies on both lines.
If two lines are not parallel, then there exists a unique point in their intersection.
Equations
- EuclidGeom.termLineInx = Lean.ParserDescr.node `EuclidGeom.termLineInx 1024 (Lean.ParserDescr.symbol "LineInx")
Instances For
def Intersection_of_Lines_of_Rays {ray₁ ray₂ : Ray P} (h : ¬ (LinearObj.ray ray₁) ∥ ray₂) : P := sorry
scoped notation "RayInx" => Intersection_of_Lines_of_Rays
theorem ray_intersection_lies_on_lines_of_rays {ray₁ ray₂ : Ray P} (h : ¬ (LinearObj.ray ray₁) ∥ ray₂) : (RayInx h) LiesOn ray₁.toLine ∧ (RayInx h) LiesOn ray₂.toLine := by sorry
-- theorem ray_intersection_eq_line_intersection_of_rays {ray₁ ray₂ : Ray P} (h : ¬ (LinearObj.ray ray₁) ∥ ray₂) : RayInt h = LineInt (Ne.trans (ray_parallel_toLine_assoc_ray ray₁) h) := sorry