Nuprl Lemma : oriented-colinear-append
∀e:OrientedPlane. ∀L1,L2:Point List.
((∃A,B:Point. (A ≠ B ∧ ((A ∈ L1) ∧ (A ∈ L2)) ∧ (B ∈ L1) ∧ (B ∈ L2)))
⇒ geo-colinear-set(e; L1)
⇒ geo-colinear-set(e; L2)
⇒ geo-colinear-set(e; L1 @ L2))
Proof
Definitions occuring in Statement :
oriented-plane: OrientedPlane,
geo-colinear-set: geo-colinear-set(e; L),
geo-sep: a ≠ b,
geo-point: Point,
l_member: (x ∈ l),
append: as @ bs,
list: T List,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
euclidean-plane: EuclideanPlane,
oriented-plane: OrientedPlane
Lemmas referenced :
geo-colinear-append
Rules used in proof :
hypothesis,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
sqequalRule,
extract_by_obid,
introduction,
cut
Latex:
\mforall{}e:OrientedPlane. \mforall{}L1,L2:Point List.
((\mexists{}A,B:Point. (A \mneq{} B \mwedge{} ((A \mmember{} L1) \mwedge{} (A \mmember{} L2)) \mwedge{} (B \mmember{} L1) \mwedge{} (B \mmember{} L2)))
{}\mRightarrow{} geo-colinear-set(e; L1)
{}\mRightarrow{} geo-colinear-set(e; L2)
{}\mRightarrow{} geo-colinear-set(e; L1 @ L2))
Date html generated:
2017_10_02-PM-04_46_35
Last ObjectModification:
2017_08_07-AM-11_10_35
Theory : euclidean!plane!geometry
Home
Index