Nuprl Lemma : geo-X_wf

e:EuclideanPlaneStructure. (X ∈ Point)


Proof




Definitions occuring in Statement :  geo-X: X euclidean-plane-structure: EuclideanPlaneStructure geo-point: Point all: x:A. B[x] member: t ∈ T
Definitions unfolded in proof :  pi2: snd(t) implies:  Q prop: exists: x:A. B[x] sq_exists: x:{A| B[x]} so_apply: x[s] so_lambda: λ2x.t[x] subtype_rel: A ⊆B uall: [x:A]. B[x] geo-X: X member: t ∈ T all: x:A. B[x]
Lemmas referenced :  euclidean-plane-structure_wf equal_wf geo-sep_wf sq_exists_wf euclidean-plane-structure-subtype geo-point_wf exists_wf geo-nontrivial_wf
Rules used in proof :  independent_functionElimination dependent_functionElimination equalitySymmetry equalityTransitivity rename setElimination productElimination because_Cache lambdaEquality sqequalRule applyEquality hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}e:EuclideanPlaneStructure.  (X  \mmember{}  Point)



Date html generated: 2017_10_02-PM-03_28_28
Last ObjectModification: 2017_08_04-PM-08_50_13

Theory : euclidean!plane!geometry


Home Index