Nuprl Lemma : generated-subspace-is-subspace
∀K:Rng. ∀vs:VectorSpace(K). ∀[P:Point(vs) ⟶ ℙ]. vs-subspace(K;vs;w.Subspace(x.P[x]) w)
Proof
Definitions occuring in Statement :
generated-subspace: Subspace(v.P[v]),
vs-subspace: vs-subspace(K;vs;x.P[x]),
vector-space: VectorSpace(K),
vs-point: Point(vs),
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
all: ∀x:A. B[x],
apply: f a,
function: x:A ⟶ B[x],
rng: Rng
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
so_lambda: λ2x.t[x],
rng: Rng,
so_apply: x[s],
implies: P ⇒ Q,
generated-subspace: Subspace(v.P[v]),
or: P ∨ Q,
prop: ℙ,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
top: Top,
exists: ∃x:A. B[x],
true: True,
squash: ↓T,
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
rev_implies: P ⇐ Q,
vs-tree-val: vs-tree-val(vs;t),
l_tree_node: l_tree_node(val;left_subtree;right_subtree),
l_tree_ind: l_tree_ind,
pi1: fst(t)
Lemmas referenced :
implies-vs-subspace,
generated-subspace_wf,
vs-point_wf,
vs-0_wf,
exists_wf,
l_tree_wf,
rng_car_wf,
equal_wf,
vs-tree-val_wf,
l_tree_covariant,
top_wf,
subtype_rel_product,
vector-space_wf,
rng_wf,
vs-mul_wf,
vs-add_wf,
vs-zero-add,
iff_weakening_equal,
vs-zero-mul,
squash_wf,
true_wf,
rng_sig_wf,
subtype_rel_self,
l_tree_node_wf,
rng_zero_wf,
vs-add-comm,
vs-mon_ident,
vs-mul-zero
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
isect_memberFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isectElimination,
sqequalRule,
lambdaEquality,
applyEquality,
setElimination,
rename,
because_Cache,
hypothesis,
independent_functionElimination,
inlFormation,
productEquality,
functionExtensionality,
independent_isectElimination,
isect_memberEquality,
voidElimination,
voidEquality,
unionElimination,
productElimination,
functionEquality,
cumulativity,
universeEquality,
equalityUniverse,
levelHypothesis,
natural_numberEquality,
equalityTransitivity,
equalitySymmetry,
imageElimination,
imageMemberEquality,
baseClosed,
instantiate,
inrFormation,
dependent_pairFormation,
hyp_replacement,
applyLambdaEquality
Latex:
\mforall{}K:Rng. \mforall{}vs:VectorSpace(K). \mforall{}[P:Point(vs) {}\mrightarrow{} \mBbbP{}]. vs-subspace(K;vs;w.Subspace(x.P[x]) w)
Date html generated:
2018_05_22-PM-09_42_17
Last ObjectModification:
2018_05_20-PM-10_42_59
Theory : linear!algebra
Home
Index