Nuprl Lemma : oal_lv_nid

s:LOSet. ∀g:AbDMon. ∀ps:|oal(s;g)|.  ((¬(ps 00 ∈ |oal(s;g)|))  (lv(ps) e ∈ |g|)))


Proof




Definitions occuring in Statement :  oal_lv: lv(ps) oal_nil: 00 oalist: oal(a;b) all: x:A. B[x] not: ¬A implies:  Q equal: t ∈ T abdmonoid: AbDMon grp_id: e grp_car: |g| loset: LOSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T so_lambda: λ2x.t[x] implies:  Q prop: uall: [x:A]. B[x] subtype_rel: A ⊆B dset: DSet abdmonoid: AbDMon dmon: DMon mon: Mon so_apply: x[s] guard: {T} false: False not: ¬A oal_nil: 00 oal_lv: lv(ps) top: Top pi2: snd(t) oal_cons_pr: oal_cons_pr(x;y;ws) loset: LOSet poset: POSet{i} qoset: QOSet set_prod: s × t mk_dset: mk_dset(T, eq) set_car: |p| pi1: fst(t) oalist: oal(a;b) dset_set: dset_set dset_list: List dset_of_mon: g↓set
Lemmas referenced :  oalist_cases_a not_wf equal_wf set_car_wf oalist_wf dset_wf oal_nil_wf grp_car_wf oal_lv_wf grp_id_wf abdmonoid_wf loset_wf reduce_hd_cons_lemma oal_cons_pr_wf assert_wf before_wf map_wf set_prod_wf dset_of_mon_wf pi1_wf_top
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality sqequalRule lambdaEquality functionEquality isectElimination hypothesis applyEquality setElimination rename independent_functionElimination because_Cache voidElimination lemma_by_obid isect_memberEquality voidEquality productElimination independent_pairEquality

Latex:
\mforall{}s:LOSet.  \mforall{}g:AbDMon.  \mforall{}ps:|oal(s;g)|.    ((\mneg{}(ps  =  00))  {}\mRightarrow{}  (\mneg{}(lv(ps)  =  e)))



Date html generated: 2019_10_16-PM-01_08_02
Last ObjectModification: 2018_08_22-AM-11_44_37

Theory : polynom_2


Home Index