Nuprl Definition : generated-subspace
Subspace(v.P[v]) == λw.((w = 0 ∈ Point(vs)) ∨ (∃t:l_tree(v:Point(vs) × P[v];|K|). (w = vs-tree-val(vs;t) ∈ Point(vs))))
Definitions occuring in Statement :
vs-tree-val: vs-tree-val(vs;t),
vs-0: 0,
vs-point: Point(vs),
l_tree: l_tree(L;T),
exists: ∃x:A. B[x],
or: P ∨ Q,
lambda: λx.A[x],
product: x:A × B[x],
equal: s = t ∈ T,
rng_car: |r|
Definitions occuring in definition :
lambda: λx.A[x],
or: P ∨ Q,
vs-0: 0,
exists: ∃x:A. B[x],
l_tree: l_tree(L;T),
product: x:A × B[x],
rng_car: |r|,
equal: s = t ∈ T,
vs-point: Point(vs),
vs-tree-val: vs-tree-val(vs;t)
FDL editor aliases :
generated-subspace
Latex:
Subspace(v.P[v]) == \mlambda{}w.((w = 0) \mvee{} (\mexists{}t:l\_tree(v:Point(vs) \mtimes{} P[v];|K|). (w = vs-tree-val(vs;t))))
Date html generated:
2018_05_22-PM-09_42_10
Last ObjectModification:
2018_01_23-PM-01_52_08
Theory : linear!algebra
Home
Index