Nuprl Lemma : oal_grp_wf2

s:LOSet. ∀g:OGrp.  (oal_grp(s;g) ∈ OGrp)


Proof




Definitions occuring in Statement :  oal_grp: oal_grp(s;g) all: x:A. B[x] member: t ∈ T ocgrp: OGrp loset: LOSet
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T subtype_rel: A ⊆B ocgrp: OGrp uall: [x:A]. B[x] ocmon: OCMon abmonoid: AbMon mon: Mon prop: squash: T omon: OMon and: P ∧ Q grp: Group{i} abgrp: AbGrp guard: {T} uimplies: supposing a cancel: Cancel(T;S;op) dmon: DMon abdmonoid: AbDMon grp_leq: a ≤ b dset: DSet dset_of_mon: g↓set set_prod: s × t dset_list: List set_car: |p| mk_dset: mk_dset(T, eq) dset_set: dset_set oalist: oal(a;b) implies:  Q infix_ap: y pi2: snd(t) grp_op: * pi1: fst(t) grp_car: |g| oal_grp: oal_grp(s;g) monot: monot(T;x,y.R[x; y];f) rev_implies:  Q iff: ⇐⇒ Q so_apply: x[s] so_lambda: λ2x.t[x] bfalse: ff uiff: uiff(P;Q) ifthenelse: if then else fi  band: p ∧b q btrue: tt it: unit: Unit bool: 𝔹 so_apply: x[s1;s2] so_lambda: λ2y.t[x; y]
Lemmas referenced :  ocgrp_wf loset_wf oal_grp_wf ocgrp_subtype_abdgrp abdgrp_subtype_abgrp oal_grp_wf1 inverse_wf grp_car_wf grp_op_wf grp_id_wf grp_inv_wf infix_ap_wf equal_wf igrp_wf grp_wf abgrp_wf subtype_rel_transitivity abgrp_subtype_grp grp_subtype_igrp grp_op_cancel_l comm_wf dmon_wf abdmonoid_wf ocmon_wf ocgrp_subtype_ocmon ocmon_subtype_abdmonoid abdmonoid_dmon abmonoid_properties ocmon_properties ocgrp_properties omon_lt_mono_imp_leq_mono dset_wf oalist_wf set_car_wf grp_lt_wf oal_merge_wf2 oal_lt_iff_grp_lt oal_merge_preserves_lt monot_wf uall_wf cancel_wf eqtt_to_assert grp_eq_wf grp_le_wf bool_wf assert_wf ulinorder_wf grp_properties abgrp_properties
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalHypSubstitution hypothesis introduction extract_by_obid dependent_functionElimination thin hypothesisEquality applyEquality sqequalRule dependent_set_memberEquality isectElimination setElimination rename because_Cache imageElimination baseClosed imageMemberEquality applyLambdaEquality equalitySymmetry equalityTransitivity independent_pairFormation axiomEquality isect_memberEquality lambdaEquality independent_isectElimination instantiate productElimination isect_memberFormation independent_functionElimination equalityElimination unionElimination functionEquality productEquality

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.    (oal\_grp(s;g)  \mmember{}  OGrp)



Date html generated: 2019_10_16-PM-01_08_49
Last ObjectModification: 2018_08_22-AM-11_53_49

Theory : polynom_2


Home Index