Nuprl Lemma : geo-SC_wf
∀[g:EuclideanPlaneStructure]
∀c,d,a:Point. ∀b:{b:Point| b # a ∧ B(cbd)} . (SC(a;b;c;d) ∈ {u:Point| cu ≅ cd ∧ B(abu) ∧ (b # d ⇒ b # u)} )
Proof
Definitions occuring in Statement :
geo-SC: SC(a;b;c;d),
euclidean-plane-structure: EuclideanPlaneStructure,
geo-congruent: ab ≅ cd,
geo-between: B(abc),
geo-sep: a # b,
geo-point: Point,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]}
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
geo-SC: SC(a;b;c;d),
and: P ∧ Q,
euclidean-plane-structure: EuclideanPlaneStructure,
record+: record+,
record-select: r.x,
subtype_rel: A ⊆r B,
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
btrue: tt,
prop: ℙ,
or: P ∨ Q,
exists: ∃x:A. B[x],
so_lambda: λ2x.t[x],
so_apply: x[s],
sq_exists: ∃x:A [B[x]],
implies: P ⇒ Q
Latex:
\mforall{}[g:EuclideanPlaneStructure]
\mforall{}c,d,a:Point. \mforall{}b:\{b:Point| b \# a \mwedge{} B(cbd)\} .
(SC(a;b;c;d) \mmember{} \{u:Point| cu \mcong{} cd \mwedge{} B(abu) \mwedge{} (b \# d {}\mRightarrow{} b \# u)\} )
Date html generated:
2020_05_20-AM-09_43_43
Last ObjectModification:
2019_12_03-AM-09_53_17
Theory : euclidean!plane!geometry
Home
Index