Nuprl Lemma : relative-free-vs_wf

[K:CRng]. ∀[S,T:Type].  relative-free-vs(K;S;T) ∈ VectorSpace(K) supposing strong-subtype(T;S)


Proof




Definitions occuring in Statement :  relative-free-vs: relative-free-vs(K;S;T) vector-space: VectorSpace(K) strong-subtype: strong-subtype(A;B) uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T universe: Type crng: CRng
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a relative-free-vs: relative-free-vs(K;S;T) so_lambda: λ2x.t[x] subtype_rel: A ⊆B vs-point: Point(vs) record-select: r.x free-vs: free-vs(K;S) mk-vs: mk-vs record-update: r[x := v] ifthenelse: if then else fi  eq_atom: =a y bfalse: ff btrue: tt formal-sum: formal-sum(K;S) quotient: x,y:A//B[x; y] crng: CRng rng: Rng so_apply: x[s] prop:
Lemmas referenced :  vs-quotient_wf free-vs_wf fs-in-subtype_wf subtype_rel_self formal-sum_wf vs-point_wf fs-in-subtype-subspace strong-subtype_wf istype-universe crng_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality because_Cache hypothesis lambdaEquality_alt independent_isectElimination applyEquality setElimination rename universeIsType axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality_alt isectIsTypeImplies inhabitedIsType instantiate universeEquality

Latex:
\mforall{}[K:CRng].  \mforall{}[S,T:Type].    relative-free-vs(K;S;T)  \mmember{}  VectorSpace(K)  supposing  strong-subtype(T;S)



Date html generated: 2019_10_31-AM-06_30_28
Last ObjectModification: 2019_08_20-AM-10_33_44

Theory : linear!algebra


Home Index