### Nuprl Lemma : bag-splits_wf

`∀T:Type. ∀b:bag(T).  (bag-splits(b) ∈ bag(bag(T) × bag(T)))`

Proof

Definitions occuring in Statement :  bag-splits: `bag-splits(b)` bag: `bag(T)` all: `∀x:A. B[x]` member: `t ∈ T` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` bag: `bag(T)` uall: `∀[x:A]. B[x]` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` implies: `P `` Q` prop: `ℙ`
Lemmas referenced :  bag_wf quotient-member-eq list_wf permutation_wf permutation-equiv bag-splits_wf_list bag-splits-permutation equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution pointwiseFunctionalityForEquality lemma_by_obid isectElimination thin productEquality hypothesisEquality hypothesis sqequalRule pertypeElimination productElimination lambdaEquality independent_isectElimination dependent_functionElimination independent_functionElimination equalityTransitivity equalitySymmetry because_Cache cumulativity universeEquality

Latex:
\mforall{}T:Type.  \mforall{}b:bag(T).    (bag-splits(b)  \mmember{}  bag(bag(T)  \mtimes{}  bag(T)))

Date html generated: 2016_05_15-PM-02_53_16
Last ObjectModification: 2015_12_27-AM-09_32_00

Theory : bags

Home Index