### Nuprl Lemma : bag-map-trivial

`∀[A:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ A].  bag-map(f;as) = as ∈ bag(A) supposing ∀x:A. ((f x) = x ∈ A)`

Proof

Definitions occuring in Statement :  bag-map: `bag-map(f;bs)` bag: `bag(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  bag: `bag(T)` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` member: `t ∈ T` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` uimplies: `b supposing a` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` bag-map: `bag-map(f;bs)` squash: `↓T` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  list_wf quotient-member-eq permutation_wf permutation-equiv equal_wf bag_wf bag-map_wf equal-wf-base all_wf squash_wf true_wf trivial_map iff_weakening_equal l_member_wf list-subtype-bag
Rules used in proof :  sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity pointwiseFunctionalityForEquality because_Cache sqequalRule pertypeElimination cut productElimination thin equalityTransitivity hypothesis equalitySymmetry introduction extract_by_obid isectElimination cumulativity hypothesisEquality lambdaFormation rename lambdaEquality independent_isectElimination dependent_functionElimination independent_functionElimination hyp_replacement applyLambdaEquality functionExtensionality applyEquality productEquality functionEquality universeEquality isect_memberFormation isect_memberEquality axiomEquality imageElimination natural_numberEquality imageMemberEquality baseClosed

Latex:
\mforall{}[A:Type].  \mforall{}[as:bag(A)].  \mforall{}[f:A  {}\mrightarrow{}  A].    bag-map(f;as)  =  as  supposing  \mforall{}x:A.  ((f  x)  =  x)

Date html generated: 2017_10_01-AM-08_46_04
Last ObjectModification: 2017_07_26-PM-04_31_06

Theory : bags

Home Index