Nuprl Lemma : geo-intersect-LINE-iff-line
∀eu:EuclideanParPlane. ∀L,M:LINE. (L \/ M ⇐⇒ ∃l:{l:Line| l = L ∈ LINE} . ∃m:{m:Line| m = M ∈ LINE} . l \/ m)
Proof
Definitions occuring in Statement :
euclidean-parallel-plane: EuclideanParPlane,
geo-intersect: L \/ M,
geoline: LINE,
geo-line: Line,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
set: {x:A| B[x]} ,
equal: s = t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
euclidean-parallel-plane: EuclideanParPlane,
prop: ℙ,
rev_implies: P ⇐ Q,
exists: ∃x:A. B[x],
subtype_rel: A ⊆r B,
guard: {T},
uimplies: b supposing a,
so_lambda: λ2x.t[x],
so_apply: x[s],
geo-intersect: L \/ M,
cand: A c∧ B,
geo-line: Line,
pi1: fst(t),
pi2: snd(t),
sq_stable: SqStable(P),
squash: ↓T,
geo-incident: p I L,
uiff: uiff(P;Q)
Latex:
\mforall{}eu:EuclideanParPlane. \mforall{}L,M:LINE. (L \mbackslash{}/ M \mLeftarrow{}{}\mRightarrow{} \mexists{}l:\{l:Line| l = L\} . \mexists{}m:\{m:Line| m = M\} . l \mbackslash{}/ m)
Date html generated:
2020_05_20-AM-10_47_24
Last ObjectModification:
2020_01_13-PM-06_05_23
Theory : euclidean!plane!geometry
Home
Index