### Nuprl Lemma : mset_for_when_unique

`∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀b:|s| ⟶ 𝔹. ∀u:|s|.`
`  ((↑b[u])`
`  `` (∀as:MSet{s}`
`        ((∀x:|s|. ((x #∈ as) ≤ 1))`
`        `` (↑(u`
`           ∈b as))`
`        `` (∀v:|s|. ((↑b[v]) `` (↑(v ∈b as)) `` (v = u ∈ |s|)))`
`        `` ((msFor{g} x ∈ as. when b[x]. f[x]) = f[u] ∈ |g|))))`

Proof

Definitions occuring in Statement :  mset_for: mset_for mset_mem: mset_mem mset_count: `x #∈ a` mset: `MSet{s}` assert: `↑b` bool: `𝔹` so_apply: `x[s]` le: `A ≤ B` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` natural_number: `\$n` equal: `s = t ∈ T` mon_when: `when b. p` iabmonoid: `IAbMonoid` grp_car: `|g|` dset: `DSet` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` member: `t ∈ T` dset: `DSet` so_lambda: `λ2x.t[x]` subtype_rel: `A ⊆r B` nat: `ℕ` so_apply: `x[s]` prop: `ℙ` iabmonoid: `IAbMonoid` imon: `IMonoid` sq_stable: `SqStable(P)` mset: `MSet{s}` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` squash: `↓T` mset_for: mset_for mset_mem: mset_mem mset_count: `x #∈ a` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  sq_stable__all all_wf set_car_wf le_wf mset_count_wf nat_wf assert_wf mset_mem_wf equal_wf grp_car_wf mset_for_wf mon_when_wf sq_stable__equal mset_wf bool_wf iabmonoid_wf dset_wf squash_wf equal-wf-base list_wf permr_wf mem_wf count_wf mon_for_when_unique distinct_iff_counts_le_one
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis sqequalRule lambdaEquality dependent_functionElimination applyEquality natural_numberEquality because_Cache functionEquality functionExtensionality independent_functionElimination pointwiseFunctionalityForEquality pertypeElimination productElimination imageMemberEquality baseClosed productEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}s:DSet.  \mforall{}g:IAbMonoid.  \mforall{}f:|s|  {}\mrightarrow{}  |g|.  \mforall{}b:|s|  {}\mrightarrow{}  \mBbbB{}.  \mforall{}u:|s|.
((\muparrow{}b[u])
{}\mRightarrow{}  (\mforall{}as:MSet\{s\}
((\mforall{}x:|s|.  ((x  \#\mmember{}  as)  \mleq{}  1))
{}\mRightarrow{}  (\muparrow{}(u
\mmember{}\msubb{}  as))
{}\mRightarrow{}  (\mforall{}v:|s|.  ((\muparrow{}b[v])  {}\mRightarrow{}  (\muparrow{}(v  \mmember{}\msubb{}  as))  {}\mRightarrow{}  (v  =  u)))
{}\mRightarrow{}  ((msFor\{g\}  x  \mmember{}  as.  when  b[x].  f[x])  =  f[u]))))

Date html generated: 2017_10_01-AM-10_00_39
Last ObjectModification: 2017_03_03-PM-01_02_20

Theory : mset

Home Index