### Nuprl Lemma : bag-union-is-single-if

`∀[T:Type]. ∀[x:T].  ∀bbs:bag(bag(T)). bag-union(bbs) = {x} ∈ bag(T) supposing bbs = {{x}} ∈ bag(bag(T))`

Proof

Definitions occuring in Statement :  bag-union: `bag-union(bbs)` single-bag: `{x}` bag: `bag(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uimplies: `b supposing a` subtype_rel: `A ⊆r B` prop: `ℙ`
Lemmas referenced :  bag-union-single single-bag_wf bag-subtype-list equal_wf bag_wf bag-union_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation hypothesis thin sqequalRule extract_by_obid sqequalHypSubstitution dependent_functionElimination cumulativity hypothesisEquality applyEquality because_Cache hyp_replacement equalitySymmetry Error :applyLambdaEquality,  isectElimination lambdaEquality isect_memberEquality axiomEquality equalityTransitivity universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].    \mforall{}bbs:bag(bag(T)).  bag-union(bbs)  =  \{x\}  supposing  bbs  =  \{\{x\}\}

Date html generated: 2016_10_25-AM-10_23_22
Last ObjectModification: 2016_07_12-AM-06_39_59

Theory : bags

Home Index