Nuprl Lemma : rv-0_wf

[rv:RealVectorSpace]. (0 ∈ Point)


Proof




Definitions occuring in Statement :  rv-0: 0 real-vector-space: RealVectorSpace ss-point: Point uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  guard: {T} all: x:A. B[x] so_apply: x[s] prop: implies:  Q so_lambda: λ2x.t[x] and: P ∧ Q btrue: tt ifthenelse: if then else fi  eq_atom: =a y record-select: r.x record+: record+ real-vector-space: RealVectorSpace rv-0: 0 subtype_rel: A ⊆B member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  real-vector-space_wf rmul_wf int-to-real_wf req_wf real_wf ss-eq_wf all_wf ss-point_wf subtype_rel_self real-vector-space_subtype1
Rules used in proof :  axiomEquality natural_numberEquality rename setElimination equalitySymmetry equalityTransitivity functionExtensionality lambdaEquality productEquality because_Cache functionEquality setEquality isectElimination tokenEquality thin dependentIntersectionEqElimination dependentIntersectionElimination sqequalRule sqequalHypSubstitution hypothesis extract_by_obid applyEquality hypothesisEquality cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[rv:RealVectorSpace].  (0  \mmember{}  Point)



Date html generated: 2016_11_08-AM-09_13_11
Last ObjectModification: 2016_10_31-PM-01_46_54

Theory : inner!product!spaces


Home Index