Nuprl Lemma : relative-vs_wf
∀[K:CRng]. ∀[vs:VectorSpace(K)]. ∀[A,B:Point(vs) ⟶ ℙ].
a.A[a]//b.B[b] ∈ VectorSpace(K)
supposing vs-subspace(K;vs;a.A[a]) ∧ vs-subspace(K;vs;b.B[b]) ∧ (∀v:Point(vs). (B[v] ⇒ A[v]))
Proof
Definitions occuring in Statement :
relative-vs: v.A[v]//z.B[z],
vs-subspace: vs-subspace(K;vs;x.P[x]),
vector-space: VectorSpace(K),
vs-point: Point(vs),
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
function: x:A ⟶ B[x],
crng: CRng
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
relative-vs: v.A[v]//z.B[z],
and: P ∧ Q,
crng: CRng,
so_lambda: λ2x.t[x],
so_apply: x[s],
subtype_rel: A ⊆r B,
rng: Rng,
all: ∀x:A. B[x],
implies: P ⇒ Q,
sub-vs: (v:vs | P[v]),
vs-0: 0,
vs-mul: a * x,
vs-add: x + y,
mk-vs: mk-vs,
top: Top,
eq_atom: x =a y,
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt,
prop: ℙ,
vs-subspace: vs-subspace(K;vs;x.P[x]),
guard: {T}
Lemmas referenced :
vs-quotient_wf,
sub-vs_wf,
sub-vs-point-subtype,
vs-point_wf,
implies-vs-subspace,
rec_select_update_lemma,
istype-void,
rng_car_wf,
vs-subspace_wf,
subtype_rel_self,
vector-space_wf,
crng_wf,
vs-add_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation_alt,
introduction,
cut,
sqequalRule,
sqequalHypSubstitution,
productElimination,
thin,
extract_by_obid,
isectElimination,
hypothesisEquality,
setElimination,
rename,
because_Cache,
hypothesis,
lambdaEquality_alt,
applyEquality,
independent_isectElimination,
universeIsType,
dependent_functionElimination,
independent_functionElimination,
isect_memberEquality_alt,
voidElimination,
lambdaFormation_alt,
axiomEquality,
equalityTransitivity,
equalitySymmetry,
productIsType,
functionIsType,
instantiate,
universeEquality,
isectIsTypeImplies,
inhabitedIsType
Latex:
\mforall{}[K:CRng]. \mforall{}[vs:VectorSpace(K)]. \mforall{}[A,B:Point(vs) {}\mrightarrow{} \mBbbP{}].
a.A[a]//b.B[b] \mmember{} VectorSpace(K)
supposing vs-subspace(K;vs;a.A[a]) \mwedge{} vs-subspace(K;vs;b.B[b]) \mwedge{} (\mforall{}v:Point(vs). (B[v] {}\mRightarrow{} A[v]))
Date html generated:
2019_10_31-AM-06_28_11
Last ObjectModification:
2019_08_12-PM-01_27_47
Theory : linear!algebra
Home
Index