Nuprl Lemma : eu-pp-prim_wf
∀[eu:EuclideanParPlane]. (pp(eu) ∈ ProjGeomPrimitives)
Proof
Definitions occuring in Statement :
eu-pp-prim: pp(eu),
euclidean-parallel-plane: EuclideanParPlane,
pgeo-primitives: ProjGeomPrimitives,
uall: ∀[x:A]. B[x],
member: t ∈ T
Definitions unfolded in proof :
all: ∀x:A. B[x],
uimplies: b supposing a,
guard: {T},
subtype_rel: A ⊆r B,
eu-pp-prim: pp(eu),
member: t ∈ T,
uall: ∀[x:A]. B[x]
Lemmas referenced :
pp-sep_wf,
unit_wf2,
geo-line_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,
geo-point_wf,
mk-pgeo-prim_wf
Rules used in proof :
equalitySymmetry,
equalityTransitivity,
axiomEquality,
lambdaEquality,
because_Cache,
dependent_functionElimination,
sqequalRule,
independent_isectElimination,
instantiate,
hypothesis,
applyEquality,
hypothesisEquality,
unionEquality,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
cut,
introduction,
isect_memberFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}[eu:EuclideanParPlane]. (pp(eu) \mmember{} ProjGeomPrimitives)
Date html generated:
2018_05_22-PM-01_16_55
Last ObjectModification:
2018_05_21-PM-03_40_41
Theory : euclidean!plane!geometry
Home
Index