Nuprl Lemma : geo-gt-prim_wf

[g:GeometryPrimitives]. ∀[a,b,c,d:Point].  (ab>cd) ∈ ℙ)


Proof




Definitions occuring in Statement :  geo-gt-prim: ab>cd) geo-primitives: GeometryPrimitives geo-point: Point uall: [x:A]. B[x] prop: member: t ∈ T
Definitions unfolded in proof :  geo-gt-prim: ab>cd) prop: so_apply: x[s] so_lambda: λ2x.t[x] btrue: tt ifthenelse: if then else fi  eq_atom: =a y subtype_rel: A ⊆B record-select: r.x record+: record+ geo-point: Point geo-primitives: GeometryPrimitives member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  geo-primitives_wf istype-atom top_wf record-select_wf subtype_rel_self
Rules used in proof :  universeIsType isectIsTypeImplies isect_memberEquality_alt inhabitedIsType axiomEquality hypothesisEquality equalitySymmetry equalityTransitivity lambdaEquality_alt cumulativity functionEquality universeEquality isectElimination extract_by_obid instantiate tokenEquality applyEquality hypothesis thin dependentIntersectionEqElimination dependentIntersectionElimination sqequalRule sqequalHypSubstitution cut introduction isect_memberFormation_alt sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[g:GeometryPrimitives].  \mforall{}[a,b,c,d:Point].    (ab>cd)  \mmember{}  \mBbbP{})



Date html generated: 2019_10_29-AM-09_11_55
Last ObjectModification: 2019_10_25-PM-01_17_53

Theory : euclidean!plane!geometry


Home Index