Nuprl Lemma : zero-bfs_wf
∀[S:Type]. ∀[K:RngSig]. ∀[ss:bag(S)].  (0 * ss ∈ basic-formal-sum(K;S))
Proof
Definitions occuring in Statement : 
zero-bfs: 0 * ss
, 
basic-formal-sum: basic-formal-sum(K;S)
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
universe: Type
, 
rng_sig: RngSig
, 
bag: bag(T)
Definitions unfolded in proof : 
basic-formal-sum: basic-formal-sum(K;S)
, 
subtype_rel: A ⊆r B
, 
zero-bfs: 0 * ss
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
Lemmas referenced : 
rng_sig_wf, 
bag_wf, 
rng_zero_wf, 
rng_car_wf, 
bag-map_wf
Rules used in proof : 
universeEquality, 
because_Cache, 
isect_memberEquality, 
equalitySymmetry, 
equalityTransitivity, 
axiomEquality, 
applyEquality, 
independent_pairEquality, 
lambdaEquality, 
cumulativity, 
hypothesis, 
hypothesisEquality, 
productEquality, 
thin, 
isectElimination, 
sqequalHypSubstitution, 
extract_by_obid, 
sqequalRule, 
cut, 
introduction, 
isect_memberFormation, 
sqequalReflexivity, 
computationStep, 
sqequalTransitivity, 
sqequalSubstitution
Latex:
\mforall{}[S:Type].  \mforall{}[K:RngSig].  \mforall{}[ss:bag(S)].    (0  *  ss  \mmember{}  basic-formal-sum(K;S))
Date html generated:
2018_05_22-PM-09_44_33
Last ObjectModification:
2018_01_08-PM-01_01_52
Theory : linear!algebra
Home
Index