Nuprl Lemma : sv-bag-is-bag-rep
∀[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,
quotient-member-eq,
list_wf,
permutation_wf,
permutation-equiv,
bag-rep_wf,
bag-size_wf,
list-subtype-bag,
bag-rep-is-single-valued,
int_seg_wf,
length_wf,
equal_wf,
inject_wf,
permute_list_wf,
bag-size-rep,
list_extensionality_iff,
squash_wf,
true_wf,
permute_list-identity,
iff_weakening_equal,
select_wf,
sq_stable__le,
permute_list_select,
less_than_transitivity1,
le_weakening,
lelt_wf,
decidable__equal_int,
less_than_wf,
false_wf,
not-equal-2,
decidable__lt,
less-iff-le,
add_functionality_wrt_le,
add-associates,
zero-add,
add-zero,
add-commutes,
le-add-cancel,
or_wf,
equal-wf-T-base,
less_than_irreflexivity,
member-bag-rep,
bag-member-select,
bag-member-sv-list,
select_member
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_30
Last ObjectModification:
2015_02_04-PM-04_46_37
Home
Index