### Nuprl Lemma : fset_for_when_eq

`∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀e:|s|. ∀as:FiniteSet{s}.`
`  ((↑(e ∈b as)) `` ((msFor{g} x ∈ as. when x (=b) e. f[x]) = f[e] ∈ |g|))`

Proof

Definitions occuring in Statement :  mset_for: mset_for mset_mem: mset_mem finite_set: `FiniteSet{s}` assert: `↑b` infix_ap: `x f y` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` equal: `s = t ∈ T` mon_when: `when b. p` iabmonoid: `IAbMonoid` grp_car: `|g|` dset: `DSet` set_eq: `=b` set_car: `|p|`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` squash: `↓T` uall: `∀[x:A]. B[x]` prop: `ℙ` iabmonoid: `IAbMonoid` imon: `IMonoid` so_lambda: `λ2x.t[x]` so_apply: `x[s]` dset: `DSet` infix_ap: `x f y` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)` uimplies: `b supposing a` finite_set: `FiniteSet{s}` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  equal_wf squash_wf true_wf grp_car_wf fset_for_when_unique set_car_wf set_eq_wf assert_of_dset_eq assert_wf mset_mem_wf iff_weakening_equal finite_set_wf iabmonoid_wf dset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination introduction extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry universeEquality setElimination rename dependent_functionElimination sqequalRule functionExtensionality because_Cache independent_functionElimination productElimination independent_isectElimination natural_numberEquality imageMemberEquality baseClosed functionEquality

Latex:
\mforall{}s:DSet.  \mforall{}g:IAbMonoid.  \mforall{}f:|s|  {}\mrightarrow{}  |g|.  \mforall{}e:|s|.  \mforall{}as:FiniteSet\{s\}.
((\muparrow{}(e  \mmember{}\msubb{}  as))  {}\mRightarrow{}  ((msFor\{g\}  x  \mmember{}  as.  when  x  (=\msubb{})  e.  f[x])  =  f[e]))

Date html generated: 2017_10_01-AM-10_00_43
Last ObjectModification: 2017_03_03-PM-01_01_59

Theory : mset

Home Index