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: 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: supposing a squash: T exists: x:A. B[x] prop: and: P ∧ Q subtype_rel: A ⊆B bag: bag(T) quotient: x,y:A//B[x; y] cand: c∧ B so_lambda: λ2x.t[x] so_apply: x[s] bag-filter: [x∈b|p[x]] all: x:A. B[x] implies:  Q iff: ⇐⇒ Q rev_implies:  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