Nuprl Lemma : eu-segments-cross
∀e:EuclideanPlane. ∀p,b,q,a:Point. ((∃c:Point. ((¬Colinear(a;b;c)) ∧ a-p-c ∧ b_q_c)) ⇒ (∃x:Point. (p-x-b ∧ q-x-a)))
Proof
Definitions occuring in Statement :
euclidean-plane: EuclideanPlane,
eu-between-eq: a_b_c,
eu-colinear: Colinear(a;b;c),
eu-between: a-b-c,
eu-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
exists: ∃x:A. B[x],
and: P ∧ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
euclidean-plane: EuclideanPlane,
prop: ℙ,
cand: A c∧ B,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
eu-inner-pasch-property,
not_wf,
eu-colinear_wf,
eu-between_wf,
eu-between-eq_wf,
eu-inner-pasch_wf,
and_wf,
exists_wf,
eu-point_wf,
euclidean-plane_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
sqequalHypSubstitution,
productElimination,
thin,
cut,
lemma_by_obid,
dependent_functionElimination,
hypothesisEquality,
isectElimination,
dependent_set_memberEquality,
because_Cache,
hypothesis,
setElimination,
rename,
dependent_pairFormation,
independent_pairFormation,
sqequalRule,
lambdaEquality
Latex:
\mforall{}e:EuclideanPlane. \mforall{}p,b,q,a:Point.
((\mexists{}c:Point. ((\mneg{}Colinear(a;b;c)) \mwedge{} a-p-c \mwedge{} b\_q\_c)) {}\mRightarrow{} (\mexists{}x:Point. (p-x-b \mwedge{} q-x-a)))
Date html generated:
2016_05_18-AM-06_33_43
Last ObjectModification:
2015_12_28-AM-09_27_47
Theory : euclidean!geometry
Home
Index