Nuprl Definition : null-formal-sum
null-formal-sum(K;S;fs) == ∃b:bag(|K| × S). ∃ss:bag(S). (fs = ((b + -(b)) + 0 * ss) ∈ bag(|K| × S))
Definitions occuring in Statement :
neg-bfs: -(fs),
zero-bfs: 0 * ss,
exists: ∃x:A. B[x],
product: x:A × B[x],
equal: s = t ∈ T,
rng_car: |r|,
bag-append: as + bs,
bag: bag(T)
Definitions occuring in definition :
exists: ∃x:A. B[x],
equal: s = t ∈ T,
bag: bag(T),
product: x:A × B[x],
rng_car: |r|,
bag-append: as + bs,
neg-bfs: -(fs),
zero-bfs: 0 * ss
FDL editor aliases :
null-formal-sum
Latex:
null-formal-sum(K;S;fs) == \mexists{}b:bag(|K| \mtimes{} S). \mexists{}ss:bag(S). (fs = ((b + -(b)) + 0 * ss))
Date html generated:
2018_05_22-PM-09_47_07
Last ObjectModification:
2018_01_08-PM-01_03_18
Theory : linear!algebra
Home
Index