Nuprl Lemma : vs-point_wf

[K:RngSig]. ∀[vs:VectorSpace(K)].  (Point(vs) ∈ Type)


Proof




Definitions occuring in Statement :  vector-space: VectorSpace(K) vs-point: Point(vs) uall: [x:A]. B[x] member: t ∈ T universe: Type rng_sig: RngSig
Definitions unfolded in proof :  infix_ap: y guard: {T} prop: all: x:A. B[x] so_apply: x[s] so_lambda: λ2x.t[x] and: P ∧ Q btrue: tt ifthenelse: if then else fi  eq_atom: =a y subtype_rel: A ⊆B record-select: r.x record+: record+ vector-space: VectorSpace(K) vs-point: Point(vs) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  rng_sig_wf vector-space_wf rng_plus_wf rng_times_wf infix_ap_wf rng_zero_wf rng_one_wf rng_car_wf equal_wf all_wf subtype_rel_self
Rules used in proof :  isect_memberEquality dependent_functionElimination axiomEquality rename setElimination hypothesisEquality functionExtensionality lambdaEquality productEquality because_Cache functionEquality setEquality equalitySymmetry equalityTransitivity universeEquality isectElimination extract_by_obid instantiate tokenEquality applyEquality hypothesis thin dependentIntersectionEqElimination dependentIntersectionElimination sqequalHypSubstitution sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[K:RngSig].  \mforall{}[vs:VectorSpace(K)].    (Point(vs)  \mmember{}  Type)



Date html generated: 2018_05_22-PM-09_40_13
Last ObjectModification: 2018_01_09-AM-10_14_58

Theory : linear!algebra


Home Index