Nuprl Lemma : stable_point-eq

[e:EuclideanPlane]. ∀[p,q:Point].  Stable{p q ∈ Point}

Proof

Definitions occuring in Statement :  euclidean-plane: EuclideanPlane eu-point: Point stable: Stable{P} uall: [x:A]. B[x] equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T stable: Stable{P} uimplies: supposing a prop: euclidean-plane: EuclideanPlane all: x:A. B[x] not: ¬A implies:  Q false: False guard: {T} sq_stable: SqStable(P) squash: T euclidean-axioms: euclidean-axioms(e) and: P ∧ Q
Lemmas referenced :  not_wf equal_wf eu-point_wf euclidean-plane_wf stable__eu-congruent eu-congruent_wf sq_stable__eu-congruent eu-congruence-identity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename because_Cache hypothesis hypothesisEquality sqequalRule isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_isectElimination lambdaFormation independent_functionElimination voidElimination hyp_replacement Error :applyLambdaEquality,  imageMemberEquality baseClosed imageElimination productElimination

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[p,q:Point].    Stable\{p  =  q\}

Date html generated: 2016_10_26-AM-07_40_52
Last ObjectModification: 2016_07_12-AM-08_06_51

Theory : euclidean!geometry

Home Index