Nuprl Lemma : bag-map-equal

[T,A:Type].
  ∀f,g:T ⟶ A. ∀P:T ⟶ 𝔹.
    ((∀x:T. ((¬↑(P x))  ((f x) (g x) ∈ A)))
     (∀as:bag(T). ((↑null([x∈as|P x]))  (bag-map(f;as) bag-map(g;as) ∈ bag(A)))))


Proof




Definitions occuring in Statement :  bag-filter: [x∈b|p[x]] bag-map: bag-map(f;bs) bag: bag(T) null: null(as) assert: b bool: 𝔹 uall: [x:A]. B[x] all: x:A. B[x] not: ¬A implies:  Q apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  bag-null: bag-null(bs) uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] implies:  Q prop: so_lambda: λ2x.t[x] so_apply: x[s] bag: bag(T) quotient: x,y:A//B[x; y] and: P ∧ Q subtype_rel: A ⊆B uimplies: supposing a bag-filter: [x∈b|p[x]] bag-map: bag-map(f;bs) nat: ge: i ≥  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top uiff: uiff(P;Q) iff: ⇐⇒ Q rev_implies:  Q cand: c∧ B int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B guard: {T} rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  assert_wf bag-null_wf bag-filter_wf bag_wf all_wf not_wf equal_wf bool_wf bag-map_wf list_wf permutation_wf equal-wf-base list-subtype-bag map_equal select_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf less_than_wf length_wf nat_wf assert_of_null filter_wf5 l_member_wf member_filter select_member lelt_wf assert_functionality_wrt_uiff eta_conv null_nil_lemma btrue_wf member-implies-null-eq-bfalse and_wf null_wf btrue_neq_bfalse
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lambdaFormation hypothesis extract_by_obid sqequalHypSubstitution isectElimination thin dependent_functionElimination setEquality cumulativity hypothesisEquality applyEquality functionExtensionality lambdaEquality functionEquality axiomEquality because_Cache isect_memberEquality independent_functionElimination pointwiseFunctionalityForEquality pertypeElimination productElimination equalityTransitivity equalitySymmetry rename productEquality independent_isectElimination setElimination unionElimination natural_numberEquality dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality independent_pairFormation computeAll dependent_set_memberEquality applyLambdaEquality

Latex:
\mforall{}[T,A:Type].
    \mforall{}f,g:T  {}\mrightarrow{}  A.  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.
        ((\mforall{}x:T.  ((\mneg{}\muparrow{}(P  x))  {}\mRightarrow{}  ((f  x)  =  (g  x))))
        {}\mRightarrow{}  (\mforall{}as:bag(T).  ((\muparrow{}null([x\mmember{}as|P  x]))  {}\mRightarrow{}  (bag-map(f;as)  =  bag-map(g;as)))))



Date html generated: 2017_10_01-AM-08_45_41
Last ObjectModification: 2017_07_26-PM-04_30_51

Theory : bags


Home Index