### Nuprl Lemma : bag-filter-no-repeats

`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[bs:bag(T)].  bag-no-repeats(T;[x∈bs|p[x]]) supposing bag-no-repeats(T;bs)`

Proof

Definitions occuring in Statement :  bag-no-repeats: `bag-no-repeats(T;bs)` bag-filter: `[x∈b|p[x]]` bag: `bag(T)` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  bag-no-repeats: `bag-no-repeats(T;bs)` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` squash: `↓T` exists: `∃x:A. B[x]` prop: `ℙ` and: `P ∧ Q` subtype_rel: `A ⊆r B` bag: `bag(T)` quotient: `x,y:A//B[x; y]` cand: `A c∧ B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` bag-filter: `[x∈b|p[x]]` all: `∀x:A. B[x]` implies: `P `` Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` respects-equality: `respects-equality(S;T)`
Lemmas referenced :  bag_to_squash_list list_wf equal_wf bag_wf list-subtype-bag no_repeats_wf permutation_wf squash_wf bag-filter_wf subtype_rel_bag assert_wf istype-assert bool_wf filter_wf5 l_member_wf no_repeats_filter no_repeats_functionality_wrt_permutation permutation_inversion respects-equality-list-bag respects-equality-trivial
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation_alt introduction cut sqequalHypSubstitution imageElimination extract_by_obid isectElimination thin hypothesisEquality productElimination promote_hyp hypothesis equalitySymmetry hyp_replacement applyLambdaEquality productEquality applyEquality because_Cache independent_isectElimination lambdaEquality_alt universeIsType rename pertypeElimination imageMemberEquality baseClosed productIsType equalityIstype inhabitedIsType setEquality setElimination setIsType isect_memberEquality_alt isectIsTypeImplies functionIsType dependent_pairFormation_alt independent_pairFormation dependent_functionElimination independent_functionElimination

Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[bs:bag(T)].    bag-no-repeats(T;[x\mmember{}bs|p[x]])  supposing  bag-no-repeats(T;bs)

Date html generated: 2020_05_20-AM-08_01_45
Last ObjectModification: 2020_01_04-PM-11_16_57

Theory : bags

Home Index