Nuprl Lemma : member-eclass-simple-comb-1

[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[F:bag(A) ─→ bag(B)]. ∀[X:EClass(A)].
  (↑e ∈b F|X|) supposing ((∀as:bag(A). ((¬↑bag-null(as))  (¬↑bag-null(F as)))) and (↑e ∈b X))


Definitions occuring in Statement :  simple-comb-1: F|X| member-eclass: e ∈b X eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-E: E assert: b uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] not: ¬A implies:  Q apply: a function: x:A ─→ B[x] universe: Type bag-null: bag-null(bs) bag: bag(T)
Lemmas :  assert-bag-null-sq subtype_rel_bag top_wf member-eclass-iff-size bag_size_empty_lemma assert_wf bag-null_wf null-bag-size assert-bag-null equal-wf-T-base bag_wf iff_transitivity bnot_wf not_wf iff_weakening_uiff assert_of_bnot member-eclass_wf simple-comb-1_wf all_wf eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf

\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[F:bag(A)  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].
    (\muparrow{}e  \mmember{}\msubb{}  F|X|)  supposing  ((\mforall{}as:bag(A).  ((\mneg{}\muparrow{}bag-null(as))  {}\mRightarrow{}  (\mneg{}\muparrow{}bag-null(F  as))))  and  (\muparrow{}e  \mmember{}\msubb{}  X))

Date html generated: 2015_07_23-AM-11_27_06
Last ObjectModification: 2015_01_28-PM-11_14_03

Home Index