Nuprl Lemma : geo-point_wf

[g:GeometryPrimitives]. (Point ∈ Type)


Proof




Definitions occuring in Statement :  geo-primitives: GeometryPrimitives geo-point: Point uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  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 axiomEquality 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].  (Point  \mmember{}  Type)



Date html generated: 2019_10_29-AM-09_11_52
Last ObjectModification: 2019_10_25-PM-00_58_25

Theory : euclidean!plane!geometry


Home Index