Nuprl Lemma : P_ptsep-apartness2
∀eu:EuclideanParPlane
((∀l,m,n:Line. (l \/ m ⇒ (l \/ n ∨ m \/ n)))
⇒ (∀p,q,r:l,m:Line//l || m. ∀P:{P:Line| p = P ∈ (l,m:Line//l || m)} . ∀Q:{Q:Line| q = Q ∈ (l,m:Line//l || m)} .
∀R:{R:Line| r = R ∈ (l,m:Line//l || m)} .
(P \/ Q ⇒ (P \/ R ∨ Q \/ R))))
Proof
Definitions occuring in Statement :
euclidean-parallel-plane: EuclideanParPlane,
geo-Aparallel: l || m,
geo-intersect: L \/ M,
geo-line: Line,
quotient: x,y:A//B[x; y],
all: ∀x:A. B[x],
implies: P ⇒ Q,
or: P ∨ Q,
set: {x:A| B[x]} ,
equal: s = t ∈ T
Definitions unfolded in proof :
so_apply: x[s],
so_apply: x[s1;s2],
so_lambda: λ2x y.t[x; y],
uimplies: b supposing a,
guard: {T},
so_lambda: λ2x.t[x],
subtype_rel: A ⊆r B,
euclidean-parallel-plane: EuclideanParPlane,
uall: ∀[x:A]. B[x],
prop: ℙ,
member: t ∈ T,
implies: P ⇒ Q,
all: ∀x:A. B[x]
Lemmas referenced :
or_wf,
all_wf,
set_wf,
subtype_quotient,
geo-Aparallel-equiv,
geoline-subtype1,
geo-Aparallel_wf,
geo-primitives_wf,
euclidean-plane-structure_wf,
euclidean-plane_wf,
euclidean-parallel-plane_wf,
subtype_rel_transitivity,
euclidean-planes-subtype,
euclidean-plane-subtype,
euclidean-plane-structure-subtype,
quotient_wf,
equal_wf,
geoline_wf,
geo-line_wf,
subtype_rel_set,
geo-intersect_wf
Rules used in proof :
independent_functionElimination,
functionEquality,
independent_isectElimination,
instantiate,
lambdaEquality,
sqequalRule,
dependent_functionElimination,
applyEquality,
hypothesisEquality,
hypothesis,
because_Cache,
rename,
setElimination,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}eu:EuclideanParPlane
((\mforall{}l,m,n:Line. (l \mbackslash{}/ m {}\mRightarrow{} (l \mbackslash{}/ n \mvee{} m \mbackslash{}/ n)))
{}\mRightarrow{} (\mforall{}p,q,r:l,m:Line//l || m. \mforall{}P:\{P:Line| p = P\} . \mforall{}Q:\{Q:Line| q = Q\} . \mforall{}R:\{R:Line| r = R\} .
(P \mbackslash{}/ Q {}\mRightarrow{} (P \mbackslash{}/ R \mvee{} Q \mbackslash{}/ R))))
Date html generated:
2018_07_29-AM-09_39_08
Last ObjectModification:
2018_06_26-PM-10_23_14
Theory : euclidean!plane!geometry
Home
Index