Nuprl Lemma : bag-mapfilter-wf2

[T,A:Type]. ∀[bs:bag(T)]. ∀[p:{b:T| b ↓∈ bs}  ⟶ 𝔹]. ∀[f:{x:{b:T| b ↓∈ bs} | ↑p[x]}  ⟶ A].
  (bag-mapfilter(f;p;bs) ∈ bag(A))


Proof




Definitions occuring in Statement :  bag-member: x ↓∈ bs bag-mapfilter: bag-mapfilter(f;P;bs) bag: bag(T) assert: b bool: 𝔹 uall: [x:A]. B[x] so_apply: x[s] member: t ∈ T set: {x:A| B[x]}  function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T prop: all: x:A. B[x] so_apply: x[s]
Lemmas referenced :  bag-mapfilter_wf bag-member_wf bag-subtype assert_wf bool_wf bag_wf
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isectElimination thin setEquality hypothesisEquality hypothesis dependent_functionElimination sqequalRule cumulativity equalityTransitivity equalitySymmetry functionEquality applyEquality because_Cache universeEquality isect_memberFormation introduction axiomEquality isect_memberEquality

Latex:
\mforall{}[T,A:Type].  \mforall{}[bs:bag(T)].  \mforall{}[p:\{b:T|  b  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:\{b:T|  b  \mdownarrow{}\mmember{}  bs\}  |  \muparrow{}p[x]\}    {}\mrightarrow{}  A].
    (bag-mapfilter(f;p;bs)  \mmember{}  bag(A))



Date html generated: 2016_05_15-PM-02_47_17
Last ObjectModification: 2015_12_27-AM-09_36_15

Theory : bags


Home Index