Nuprl Lemma : oalist_hgrp_eqs

s:LOSet. ∀g:OGrp. ∀a1,a2:|oal(s;g↓hgrp)|.  ((a1 a2 ∈ |oal(s;g)|)  (a1 a2 ∈ |oal(s;g↓hgrp)|))


Proof




Definitions occuring in Statement :  oalist: oal(a;b) all: x:A. B[x] implies:  Q equal: t ∈ T hgrp_of_ocgrp: g↓hgrp ocgrp: OGrp loset: LOSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] subtype_rel: A ⊆B guard: {T} uimplies: supposing a and: P ∧ Q cand: c∧ B grp_id: e pi1: fst(t) pi2: snd(t) hgrp_of_ocgrp: g↓hgrp grp_car: |g| hgrp_car: |g|+ ocgrp: OGrp ocmon: OCMon abmonoid: AbMon mon: Mon so_lambda: λ2x.t[x] so_apply: x[s] dset: DSet
Lemmas referenced :  equal_wf set_car_wf oalist_wf ocmon_subtype_abdmonoid ocgrp_subtype_ocmon subtype_rel_transitivity ocgrp_wf ocmon_wf abdmonoid_wf set_car_inc hgrp_of_ocgrp_wf2 loset_wf oalist_strong-subtype grp_id_wf hgrp_of_ocgrp_wf grp_car_wf grp_leq_wf strong-subtype-self strong-subtype-set3 strong-subtype-implies dset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin dependent_functionElimination hypothesisEquality applyEquality instantiate independent_isectElimination sqequalRule because_Cache independent_pairFormation lambdaEquality setElimination rename independent_functionElimination equalityTransitivity equalitySymmetry

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.  \mforall{}a1,a2:|oal(s;g\mdownarrow{}hgrp)|.    ((a1  =  a2)  {}\mRightarrow{}  (a1  =  a2))



Date html generated: 2016_05_16-AM-08_22_29
Last ObjectModification: 2015_12_28-PM-06_26_42

Theory : polynom_2


Home Index