Nuprl Lemma : sv-bag-is-bag-rep-lousy-proof
∀[A:Type]. ∀[as:bag(A)]. ∀a:A. (a ↓∈ as ⇒ (as = bag-rep(#(as);a) ∈ bag(A))) supposing single-valued-bag(as;A)
Proof
Definitions occuring in Statement :
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type,
equal: s = t ∈ T,
single-valued-bag: single-valued-bag(b;T),
bag-member: x ↓∈ bs,
bag-rep: bag-rep(n;x),
bag-size: #(bs),
bag: bag(T)
Lemmas :
single-valued-bag-sv-list,
single-valued-bag-is-list,
bag-member-sv-list,
bag-rep-is-single-valued,
bag-size_wf,
list-subtype-bag,
bag-rep_wf,
l_member_wf,
the-member-bag-rep,
bag-size-rep,
nat_wf,
subtype_base_sq,
int_subtype_base,
bag-member-iff-size,
bag-member_wf,
select_wf,
sq_stable__le,
less_than_transitivity1,
length_wf,
le_weakening,
select_member,
lelt_wf,
squash_wf,
true_wf,
select-bag-rep,
iff_weakening_equal,
less_than_wf,
list_extensionality,
bag_wf,
equal_wf
Latex:
\mforall{}[A:Type]. \mforall{}[as:bag(A)].
\mforall{}a:A. (a \mdownarrow{}\mmember{} as {}\mRightarrow{} (as = bag-rep(\#(as);a))) supposing single-valued-bag(as;A)
Date html generated:
2015_07_23-AM-11_26_35
Last ObjectModification:
2015_02_04-PM-04_46_13
Home
Index