Nuprl Lemma : sq_stable__circle-strict-overlap

[g:GeometryPrimitives]. ∀[a,b,c,d:Point].  SqStable(StrictOverlap(a;b;c;d))


Proof




Definitions occuring in Statement :  circle-strict-overlap: StrictOverlap(a;b;c;d) geo-primitives: GeometryPrimitives geo-point: Point sq_stable: SqStable(P) uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T circle-strict-overlap: StrictOverlap(a;b;c;d) so_lambda: λ2x.t[x] prop: and: P ∧ Q so_apply: x[s] sq_stable: SqStable(P) implies:  Q squash: T
Lemmas referenced :  sq_stable__squash exists_wf geo-point_wf geo-congruent_wf geo-gt_wf squash_wf circle-strict-overlap_wf geo-primitives_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalRule lambdaEquality because_Cache productEquality dependent_functionElimination imageElimination imageMemberEquality baseClosed isect_memberEquality

Latex:
\mforall{}[g:GeometryPrimitives].  \mforall{}[a,b,c,d:Point].    SqStable(StrictOverlap(a;b;c;d))



Date html generated: 2017_10_02-PM-03_26_18
Last ObjectModification: 2017_08_12-PM-06_14_32

Theory : euclidean!plane!geometry


Home Index